--- a/lib/scripts/run-polyml Mon Jun 22 15:18:02 1998 +0200
+++ b/lib/scripts/run-polyml Mon Jun 22 15:25:06 1998 +0200
@@ -16,12 +16,24 @@
exit 2
}
+function check_mlhome_file()
+{
+ if [ ! -f "$1" ]; then
+ echo "Unable to locate $1" >&2
+ echo "Please check your ML_HOME setting!" >&2
+ exit 2
+ fi
+}
+
## Poly/ML programs
POLY=$ML_HOME/poly
DISCGARB=$ML_HOME/discgarb
+check_mlhome_file "$POLY"
+check_mlhome_file "$DISCGARB"
+
case "$ML_SYSTEM" in
polyml-3.*)
DISCGARB="$DISCGARB -c"
@@ -35,6 +47,7 @@
if [ -z "$INFILE" ]; then
INFILE="$ML_HOME/ML_dbase"
+ check_mlhome_file "$INFILE"
MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT"
COPYDB=""
fi