equal
deleted
inserted
replaced
78 FEEDER_OPTS="-q" |
78 FEEDER_OPTS="-q" |
79 fi |
79 fi |
80 |
80 |
81 if [ "$PRG" = "$POLY" ]; then |
81 if [ "$PRG" = "$POLY" ]; then |
82 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
82 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
83 { read FPID; "$PRG" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
83 { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
84 else |
84 else |
85 "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \ |
85 "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \ |
86 { read FPID; "$PRG" $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
86 { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
87 fi |
87 fi |
88 RC="$?" |
88 RC="$?" |
89 |
89 |
90 if [ -n "$OUTFILE" ]; then |
90 if [ -n "$OUTFILE" ]; then |
91 if [ -e "${OUTFILE}.o" ]; then |
91 if [ -e "${OUTFILE}.o" ]; then |