# HG changeset patch
# User wenzelm
# Date 850915887 -3600
# Node ID b3ac45aba238a10e904e6d65bf0892887b83c823
# Parent  e73cb5924261bb5b159294f377b11df2038f1060
fixed EXIT def;

diff -r e73cb5924261 -r b3ac45aba238 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