lib/scripts/run-smlnj
changeset 59344 e0ce214303c1
parent 56627 cb912b7de3cf
--- 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=""