equal
deleted
inserted
replaced
50 |
50 |
51 if [ -z "$OUTFILE" ]; then |
51 if [ -z "$OUTFILE" ]; then |
52 COMMIT='fun commit () = false;' |
52 COMMIT='fun commit () = false;' |
53 MLEXIT="" |
53 MLEXIT="" |
54 else |
54 else |
55 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);" |
55 if [ -z "$INFILE" ]; then |
|
56 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);" |
|
57 else |
|
58 COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");" |
|
59 fi |
56 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
60 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
57 MLEXIT="commit();" |
61 MLEXIT="commit();" |
58 fi |
62 fi |
59 |
63 |
60 |
64 |