5 # Minimalist version of cleanup, used for signal handling.
6 # Sends a SIGKILL to the entire process group, including ourselves.
7 # Needs just two external commands, making it more
8 # robust in case of resource issues.
10 echo "$0(pid $$): Caught a signal, emergency clean-up"
11 # use "pgid:1=" output format to get unpadded process group ID
12 group_id=`ps -p $$ -o pgid:1=`
13 echo "$0(pid $$): sending kill to process group ID:${group_id}"
14 kill -9 -- -${group_id}
18 # Happy camper leisurely clean up - send the signal only to other
19 # processes in the process group, and also check
20 # that the processes exists before sending the signal.
22 group_id=`ps -p $$ -o pgid=`
24 ids=`pgrep -g $group_id -d ' ' | sed "s/\b$my_id\b//g"`
25 echo "Killing possible remaining process IDs: $ids"
28 if ps -p $id > /dev/null
36 trap "panic;" SIGINT SIGTERM
44 if [[ "${FORCE_FOREGROUND}" == "1" ]]