# HG changeset patch
# User wenzelm
# Date 898521906 -7200
# Node ID d45ec8d00ab031eaacf6a306560b77f1cf67538a
# Parent  fbdb0b5413145b96ed516dd072316c9099a52509
check_mlhome_file;

diff -r fbdb0b541314 -r d45ec8d00ab0 lib/scripts/run-polyml
--- 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
diff -r fbdb0b541314 -r d45ec8d00ab0 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Mon Jun 22 15:18:02 1998 +0200
+++ b/lib/scripts/run-smlnj	Mon Jun 22 15:25:06 1998 +0200
@@ -16,6 +16,25 @@
   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
+}
+
+
+## compiler binaries
+
+SML="$ML_HOME/sml"
+ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
+
+check_mlhome_file "$SML"
+check_mlhome_file "$ARCH_N_OPSYS"
+
+
 
 ## prepare databases
 
@@ -47,14 +66,14 @@
 fi
 
 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; $ML_HOME/sml $ML_OPTIONS $DB; RC=$?; kill -HUP $FPID; exit $RC; }
+  { read FPID; $SML $ML_OPTIONS $DB; RC=$?; kill -HUP $FPID; exit $RC; }
 RC=$?
 
 
 ## fix heap file name and permissions
 
 if [ -n "$OUTFILE" ]; then
-  eval $($ML_HOME/.arch-n-opsys)
+  eval $($ARCH_N_OPSYS)
   SUFFIX=".$ARCH-$OPSYS"
   if [ -f "$OUTFILE$SUFFIX" ]; then
     mv "$OUTFILE$SUFFIX" "$OUTFILE"
diff -r fbdb0b541314 -r d45ec8d00ab0 lib/scripts/run-smlnj-0.93
--- a/lib/scripts/run-smlnj-0.93	Mon Jun 22 15:18:02 1998 +0200
+++ b/lib/scripts/run-smlnj-0.93	Mon Jun 22 15:25:06 1998 +0200
@@ -16,11 +16,21 @@
   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
+}
+
 
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
   INFILE="$ML_HOME/sml"
+  check_mlhome_file "$INFILE"
   EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;"
 else
   EXIT=""