3 # Simple function used by run_*.sh scripts
8 if [ -z "${!name}" ]; then
9 echo "$0: $name must be set"
13 [ $failed ] && exit 1 || true
16 echoerr () { echo "$@" 1>&2 ; }
19 echoerr "$(date +'%F %H:%M:%S'): client load was signaled to terminate"
21 local PGID=$(ps -eo "%c %p %r" | awk "/ $PPID / {print \$3}")