diff options
| -rwxr-xr-x | bin/common-functions.sh | 2 | ||||
| -rwxr-xr-x | bin/setsid.py | 16 |
2 files changed, 17 insertions, 1 deletions
diff --git a/bin/common-functions.sh b/bin/common-functions.sh index 7664337b..fd524d44 100755 --- a/bin/common-functions.sh +++ b/bin/common-functions.sh @@ -24,7 +24,7 @@ if [ "${0:0:5}" != "/tmp/" ] ; then # this hack makes it possible to overwrite long running scripts # anytime...) echo "$(date) - start running \"$0\" as \"$TTT\" using \"$@\" as arguments." - $TTT "$@" + /srv/jenkins/bin/setsid.py $TTT "$@" exit $? # cleanup is done automatically via trap else diff --git a/bin/setsid.py b/bin/setsid.py new file mode 100755 index 00000000..32002ec7 --- /dev/null +++ b/bin/setsid.py @@ -0,0 +1,16 @@ +#!/usr/bin/python +"""backport of util-linux' setsid -w to Debian stable""" + +import os +import sys + +if __name__ == "__main__": + assert len(sys.argv) > 1 + pid = os.fork() + if pid == 0: + os.setsid() + os.execvp(sys.argv[1], sys.argv[1:]) + else: + cpid, status = os.wait() + assert cpid == pid + sys.exit(os.WEXITSTATUS(status)) |