back to feeder -- Isabelle ML setup no longer evaluates command line;
authorwenzelm
Mon Mar 24 18:35:39 2008 +0100 (2008-03-24 ago)
changeset 26375234f10289d97
parent 26374 be47e9a83b4f
child 26376 1aeabd85866a
back to feeder -- Isabelle ML setup no longer evaluates command line;
lib/scripts/run-polyml-5.0
     1.1 --- a/lib/scripts/run-polyml-5.0	Mon Mar 24 17:09:34 2008 +0100
     1.2 +++ b/lib/scripts/run-polyml-5.0	Mon Mar 24 18:35:39 2008 +0100
     1.3 @@ -76,13 +76,8 @@
     1.4    FEEDER_OPTS="-q"
     1.5  fi
     1.6  
     1.7 -if [ "$PRG" = "$POLY" ]; then
     1.8 -  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
     1.9 -    { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.10 -else
    1.11 -  "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
    1.12 -    { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.13 -fi
    1.14 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    1.15 +  { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.16  RC="$?"
    1.17  
    1.18  if [ -n "$OUTFILE" ]; then