2017-08-11 10:06:15 +02:00
|
|
|
#!/bin/bash
|
|
|
|
|
|
|
|
if [[ "$1" == "1" ]]
|
|
|
|
then
|
|
|
|
setsid scripts/run_in_venv_with_cleanup.sh $*
|
|
|
|
else
|
|
|
|
setsid scripts/run_in_venv_with_cleanup.sh $* &
|
|
|
|
pid=$!
|
|
|
|
trap "echo setsid_wrapper.sh: got signal, killing child pid ${pid}; kill ${pid}; sleep .1;" SIGINT SIGTERM
|
2017-08-16 16:38:10 +02:00
|
|
|
wait ${pid}
|
|
|
|
exit $?
|
2017-08-11 10:06:15 +02:00
|
|
|
fi
|