back to feeder -- Isabelle ML setup no longer evaluates command line;
authorwenzelm
Mon, 24 Mar 2008 18:35:39 +0100
changeset 26375 234f10289d97
parent 26374 be47e9a83b4f
child 26376 1aeabd85866a
back to feeder -- Isabelle ML setup no longer evaluates command line;
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