mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-16 01:43:35 +00:00
76dbe913e2
scripts: Rename *.sh as *.in. The scripts are now made by configure, not by make/mmake in the scripts directory.
33 lines
797 B
Bash
33 lines
797 B
Bash
#!/bin/sh
|
|
#---------------------------------------------------------------------------#
|
|
# Copyright (C) 1995 University of Melbourne.
|
|
# This file may only be copied under the terms of the GNU General
|
|
# Public License - see the file COPYING in the Mercury distribution.
|
|
#---------------------------------------------------------------------------#
|
|
#
|
|
# mint - Mercury interface browser.
|
|
#
|
|
# Usage: mint module-name ...
|
|
|
|
INTDIR=${MERCURY_INT_DIR=@LIBDIR@/ints}
|
|
|
|
exit_status=0
|
|
|
|
if [ $# -lt 1 ]
|
|
then
|
|
echo "usage: `basename $0` module-name ..." 1>&2
|
|
exit 1
|
|
fi
|
|
|
|
for arg in "$@"; do
|
|
module="`basename $arg .nl`"
|
|
file="$INTDIR/$module.int"
|
|
if [ -r "$file" ]; then
|
|
${PAGER=more} "$file"
|
|
else
|
|
echo "`basename $0`: no interface file for \`$module'." 1>&2
|
|
exit_status=1
|
|
fi
|
|
done
|
|
exit $exit_status
|