equal
deleted
inserted
replaced
78 else |
78 else |
79 FEEDER_OPTS="-q" |
79 FEEDER_OPTS="-q" |
80 fi |
80 fi |
81 |
81 |
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; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
83 { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
84 RC="$?" |
84 RC="$?" |
85 |
85 |
86 |
86 |
87 ## fix heap file name and permissions |
87 ## fix heap file name and permissions |
88 |
88 |