--- a/lib/scripts/run-polyml-5.0 Fri Dec 08 23:25:50 2006 +0100
+++ b/lib/scripts/run-polyml-5.0 Fri Dec 08 23:25:52 2006 +0100
@@ -44,10 +44,11 @@
## prepare databases
if [ -z "$INFILE" ]; then
+ PRG="$POLY"
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
else
check_file "$INFILE"
- POLY="$INFILE"
+ PRG="$INFILE"
EXIT=""
fi
@@ -77,8 +78,13 @@
FEEDER_OPTS="-q"
fi
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+if [ "$PRG" = "$POLY" ]; then
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$PRG" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+else
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$PRG" $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+fi
RC="$?"
if [ -n "$OUTFILE" ]; then