diff --git a/all.sh b/all.sh index abd36bd..997859e 100755 --- a/all.sh +++ b/all.sh @@ -1,7 +1,6 @@ #!/bin/sh set -e -# From https://stackoverflow.com/a/360275 kill_child_jobs() { echo "In kill_child_jobs()..." # Workaround for https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=482999