potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;
--- a/lib/scripts/run-polyml Fri May 25 13:23:43 2012 +0200
+++ b/lib/scripts/run-polyml Fri May 25 17:14:14 2012 +0200
@@ -74,7 +74,7 @@
fi
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+ { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
RC="$?"
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
--- 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="$?"