equal
deleted
inserted
replaced
51 |
51 |
52 if [ -z "$OUTFILE" ]; then |
52 if [ -z "$OUTFILE" ]; then |
53 COMMIT='fun commit () = false;' |
53 COMMIT='fun commit () = false;' |
54 MLEXIT="" |
54 MLEXIT="" |
55 else |
55 else |
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);" |
56 if [ -z "$INFILE" ]; then |
|
57 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);" |
|
58 else |
|
59 COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");" |
|
60 fi |
57 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
61 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
58 MLEXIT="commit();" |
62 MLEXIT="commit();" |
59 fi |
63 fi |
60 |
64 |
61 |
65 |