equal
deleted
inserted
replaced
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 |