diff options
Diffstat (limited to 'test/scripts/run_in_venv_with_cleanup.sh')
| -rwxr-xr-x | test/scripts/run_in_venv_with_cleanup.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test/scripts/run_in_venv_with_cleanup.sh b/test/scripts/run_in_venv_with_cleanup.sh index af32f87ea5d..e87afde1ddc 100755 --- a/test/scripts/run_in_venv_with_cleanup.sh +++ b/test/scripts/run_in_venv_with_cleanup.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash rv=0 @@ -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 |