diff -r 6532efd66a70 -r cb912b7de3cf lib/scripts/run-polyml --- a/lib/scripts/run-polyml Mon Apr 21 21:16:05 2014 +0200 +++ b/lib/scripts/run-polyml Tue Apr 22 11:47:57 2014 +0200 @@ -41,7 +41,7 @@ if [ -z "$INFILE" ]; then INIT="" - EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);" + EXIT="fun exit rc = 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 exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"