lib/scripts/run-polyml
changeset 56627 cb912b7de3cf
parent 53657 64942a1f7187
child 59344 e0ce214303c1
--- 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));"