equal
deleted
inserted
replaced
40 |
40 |
41 ## prepare databases |
41 ## prepare databases |
42 |
42 |
43 if [ -z "$INFILE" ]; then |
43 if [ -z "$INFILE" ]; then |
44 INIT="" |
44 INIT="" |
45 EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);" |
45 EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);" |
46 else |
46 else |
47 check_file "$INFILE" |
47 check_file "$INFILE" |
48 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));" |
48 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));" |
49 EXIT="" |
49 EXIT="" |
50 fi |
50 fi |