diff -r 22d5c010ef5c -r 2ef891f99d2c lib/scripts/run-polyml --- a/lib/scripts/run-polyml Wed Feb 13 13:31:38 2013 +0100 +++ b/lib/scripts/run-polyml Wed Feb 13 13:52:06 2013 +0100 @@ -49,7 +49,7 @@ EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);" else check_file "$INFILE" - INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));" + INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));" EXIT="" fi @@ -57,7 +57,7 @@ COMMIT='fun commit () = false;' MLEXIT="" else - COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" + 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);" [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } MLEXIT="commit();" fi