lib/scripts/run-polyml-5.5.1
changeset 52833 21843a4c6ba9
parent 52832 980ca3d6ded4
child 52835 0906c00bb21d
equal deleted inserted replaced
52832:980ca3d6ded4 52833:21843a4c6ba9
    69 else
    69 else
    70   if [ -z "$TERMINATE" ]; then
    70   if [ -z "$TERMINATE" ]; then
    71     FEEDER_OPTS=""
    71     FEEDER_OPTS=""
    72   else
    72   else
    73     FEEDER_OPTS="-q"
    73     FEEDER_OPTS="-q"
       
    74     ML_OPTIONS="$ML_OPTIONS --error-exit"
    74   fi
    75   fi
    75   "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    76   "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    76     { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    77     { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    77   RC="$?"
    78   RC="$?"
    78 fi
    79 fi