1
0
Fork 0

Switch to much simpler solution for zsh only.

master
Daniel Perelman 4 years ago
parent 67ff44f4ed
commit 373db13c20

@ -4,27 +4,14 @@ set -e
# From https://stackoverflow.com/a/360275
kill_child_jobs() {
echo "In kill_child_jobs()..."
tmp="$(mktemp)"
# 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/gpi' | while read -r child
do
echo Killing job "$child"
builtin kill "$child" || true
done
rm "$tmp"
# From https://unix.stackexchange.com/a/544167
while kill %% >/dev/null; do :; done
}
cleanup() {
kill_child_jobs
}
#trap "kill_child_jobs" INT TERM QUIT
#trap date INT TERM QUIT
# From https://unix.stackexchange.com/a/240736
for sig in INT QUIT HUP TERM ALRM USR1; do
trap "

Loading…
Cancel
Save