diff -r 1776b55f8d7a -r 34952c2423c6 lib/scripts/run-smlnj --- 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=""