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