fixed EXIT def;
authorwenzelm
Wed, 18 Dec 1996 14:31:27 +0100
changeset 2440 b3ac45aba238
parent 2439 e73cb5924261
child 2441 decc46a5cdb5
fixed EXIT def;
lib/scripts/run-smlnj-0.93
--- a/lib/scripts/run-smlnj-0.93	Wed Dec 18 13:32:29 1996 +0100
+++ b/lib/scripts/run-smlnj-0.93	Wed Dec 18 14:31:27 1996 +0100
@@ -19,9 +19,13 @@
 
 ## prepare databases
 
-EXIT="val exit = System.Unsafe.CInterface.exit;"
+if [ -z "$INFILE" ]; then
+  INFILE="$ML_HOME/sml"
+  EXIT="val exit = System.Unsafe.CInterface.exit;"
+else
+  EXIT=""
+fi
 
-[ -z "$INFILE" ] && INFILE="$ML_HOME/sml"
 MOVE=""
 
 if [ -z "$OUTFILE" ]; then