potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;
authorwenzelm
Fri, 25 May 2012 17:14:14 +0200
changeset 48002 6de952f4069f
parent 48001 c79adcae9869
child 48003 1d11af40b106
potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;
lib/scripts/run-polyml
lib/scripts/run-smlnj
--- 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="$?"