equal
deleted
inserted
replaced
72 else |
72 else |
73 FEEDER_OPTS="-q" |
73 FEEDER_OPTS="-q" |
74 fi |
74 fi |
75 |
75 |
76 "$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 | \ |
77 { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
77 { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
78 RC="$?" |
78 RC="$?" |
79 |
79 |
80 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
80 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
81 |
81 |
82 exit "$RC" |
82 exit "$RC" |