diff -r 9e2a65912111 -r 860cd901ab43 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Thu Mar 03 15:23:02 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.6.
-
-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\""
-}
-
-
-## heap file
-
-if [ -z "$HEAP_FILE" ]; then
-  case "$ML_PLATFORM" in
-    *-windows)
-      INIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
-      ;;
-    *)
-      INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-      ;;
-  esac
-else
-  check_file "$HEAP_FILE"
-  case "$ML_PLATFORM" in
-    *-windows)
-      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
-      ;;
-    *)
-      PLATFORM_HEAP_FILE="$HEAP_FILE"
-      ;;
-  esac
-  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);"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -n "$TERMINATE" ]; then
-  "$ML_HOME/poly" -q -i $ML_OPTIONS \
-    --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$ML_TEXT")" \
-    --error-exit </dev/null
-  RC="$?"
-else
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" | \
-    { read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-  RC="$?"
-fi
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100: