diff -r 43281cd62cb0 -r e0ce214303c1 lib/scripts/run-smlnj --- a/lib/scripts/run-smlnj Sat Jan 10 20:28:53 2015 +0100 +++ b/lib/scripts/run-smlnj Sat Jan 10 21:22:25 2015 +0100 @@ -62,22 +62,20 @@ fi if [ -z "$OUTFILE" ]; then - COMMIT='fun commit () = false;' MLEXIT="" else if [ -z "$INFILE" ]; then - COMMIT="fun commit () = if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};" + MLEXIT="if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};" else - COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");" + MLEXIT="Session.save \"$OUTFILE\";" fi [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } - MLEXIT="commit();" fi ## run it! -MLTEXT="$EXIT $COMMIT $MLTEXT" +MLTEXT="$EXIT $MLTEXT" if [ -z "$TERMINATE" ]; then FEEDER_OPTS=""