lib/scripts/run-polyml
changeset 62485 a04e26352106
parent 62475 43e64c770f28
equal deleted inserted replaced
62484:4759dbb35148 62485:a04e26352106
    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