lib/scripts/run-smlnj-0.93
changeset 9789 7e5e6c47c0b5
parent 5063 d45ec8d00ab0
child 9977 32955afeb835
--- a/lib/scripts/run-smlnj-0.93	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/run-smlnj-0.93	Fri Sep 01 17:54:58 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # SML/NJ startup script (for 0.93).
 #
@@ -43,7 +45,7 @@
 else
   if [ "$INFILE" -ef "$OUTFILE" ]; then
     OUTDIR=$(dirname "$OUTFILE")/tmp
-    OUTFILE=$OUTDIR/$(basename "$OUTFILE")
+    OUTFILE="$OUTDIR"/$(basename "$OUTFILE")
     mkdir -p "$OUTDIR" || fail_out
     MOVE=true
   fi
@@ -63,9 +65,9 @@
   FEEDER_OPTS="-q"
 fi
 
-$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; $INFILE $ML_OPTIONS; RC=$?; kill -HUP $FPID; exit $RC; }
-RC=$?
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
 
 
 ## fix heap file
@@ -77,4 +79,4 @@
   mv "$OUTFILE" "$INFILE" || fail_out
 fi
 
-exit $RC
+exit "$RC"