lib/scripts/run-smlnj
changeset 39619 34952c2423c6
parent 31317 1f5740424c69
child 40544 34e56a6668ba
--- a/lib/scripts/run-smlnj	Wed Sep 22 21:21:04 2010 +0200
+++ b/lib/scripts/run-smlnj	Wed Sep 22 22:14:25 2010 +0200
@@ -57,17 +57,18 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
+  COMMIT='fun commit () = false;'
+  MLEXIT=""
 else
   COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
 MLTEXT="$EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
 
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""