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