diff options
Diffstat (limited to 'test/scripts/run_in_venv_with_cleanup.sh')
| -rwxr-xr-x | test/scripts/run_in_venv_with_cleanup.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/scripts/run_in_venv_with_cleanup.sh b/test/scripts/run_in_venv_with_cleanup.sh index 3f9d44ff4b5..e87afde1ddc 100755 --- a/test/scripts/run_in_venv_with_cleanup.sh +++ b/test/scripts/run_in_venv_with_cleanup.sh @@ -21,7 +21,9 @@ panic() { atexit() { group_id=`ps -p $$ -o pgid=` my_id=$$ - ids=`pgrep -g $group_id -d ' ' | sed "s/\b$my_id\b//g"` + SED=`which gsed` + SED=$(basename "${SED:-sed}") + ids=`pgrep -g $group_id -d ' ' | ${SED} "s/\b$my_id\b//g"` echo "Killing possible remaining process IDs: $ids" for id in $ids do |