mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-17 23:05:21 +00:00
34 lines
821 B
Bash
34 lines
821 B
Bash
#! /bin/sh
|
|
# @configure_input@
|
|
#---------------------------------------------------------------------------#
|
|
# Copyright (C) 1995 The 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 .m`"
|
|
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
|