wrappercheck.sh: more resilient against race conditions

Killing the helper shell may fail when the shell already quit.
This commit is contained in:
Patrick Ohly 2013-03-04 07:31:57 -08:00
parent 748618d6e3
commit e1317c149c

View file

@ -60,8 +60,14 @@ kill -INT $BACKGROUND_PID && kill -TERM $BACKGROUND_PID || true
KILL_PID=$!
set +e
wait $BACKGROUND_PID
kill -KILL $KILL_PID
msg=$(kill -KILL $KILL_PID 2>&1)
SUBRET=$?
if echo "$msg" | grep -q 'No such process'; then
# Consider this a success.
SUBRET=0
else
echo "$msg"
fi
set -e
if [ $RET = 0 ]; then
RET=$SUBRET