# HG changeset patch
# User wenzelm
# Date 1206380139 -3600
# Node ID 234f10289d97dcfe5ec76e9f051816686a15536d
# Parent  be47e9a83b4f8a2a7bf0d601fd6055ee2fd05da6
back to feeder -- Isabelle ML setup no longer evaluates command line;

diff -r be47e9a83b4f -r 234f10289d97 lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0	Mon Mar 24 17:09:34 2008 +0100
+++ b/lib/scripts/run-polyml-5.0	Mon Mar 24 18:35:39 2008 +0100
@@ -76,13 +76,8 @@
   FEEDER_OPTS="-q"
 fi
 
-if [ "$PRG" = "$POLY" ]; then
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-else
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-fi
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"
 
 if [ -n "$OUTFILE" ]; then