| changeset 48002 | 6de952f4069f |
| parent 40544 | 34e56a6668ba |
| child 48662 | b171bcd5dd86 |
--- a/lib/scripts/run-smlnj Fri May 25 13:23:43 2012 +0200 +++ b/lib/scripts/run-smlnj Fri May 25 17:14:14 2012 +0200 @@ -80,7 +80,7 @@ fi "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ - { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } + { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } RC="$?"