--- 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