--- a/lib/scripts/run-polyml-5.3.0 Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.3.0.
-
-export -n HEAP_FILE ML_TEXT TERMINATE
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function check_file()
-{
- [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## prepare databases
-
-if [ -z "$HEAP_FILE" ]; then
- INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
- check_file "$HEAP_FILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); Posix.Process.exit 0w1));"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" $FEEDER_OPTS | \
- { read FPID; "$ML_HOME/poly" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100: