equal
deleted
inserted
replaced
41 ;; |
41 ;; |
42 *) |
42 *) |
43 PLATFORM_HEAP_FILE="$HEAP_FILE" |
43 PLATFORM_HEAP_FILE="$HEAP_FILE" |
44 ;; |
44 ;; |
45 esac |
45 esac |
46 INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success));" |
46 INIT="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success);" |
47 fi |
47 fi |
48 |
48 |
49 |
49 |
50 ## poly process |
50 ## poly process |
51 |
51 |