You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
33 lines
835 B
Bash
33 lines
835 B
Bash
#!/bin/sh
|
|
set -e
|
|
|
|
kill_child_jobs() {
|
|
echo "In kill_child_jobs()..."
|
|
# Workaround for https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=482999
|
|
tmp="$(mktemp)"
|
|
jobs -p > "$tmp"
|
|
child_pids=$(cat "$tmp")
|
|
for child in $child_pids
|
|
do
|
|
# From https://unix.stackexchange.com/a/574169
|
|
if [ -n "${child##*[!0-9]*}" ]
|
|
then
|
|
echo Killing "$child"
|
|
# From https://stackoverflow.com/a/11231970
|
|
kill "$child" || true
|
|
fi
|
|
done
|
|
|
|
# zsh version from https://stackoverflow.com/a/36354483
|
|
# zsh doesn't have jobs -p
|
|
jobs > "$tmp"
|
|
cat "$tmp"
|
|
<"$tmp" sed --regexp-extended --quiet 's/\[([[:digit:]]+)\].*running.*/%\1/gp' | while read -r child
|
|
do
|
|
echo Killing job "$child"
|
|
kill "$child" || true
|
|
done
|
|
|
|
rm "$tmp"
|
|
}
|