diff options
-rwxr-xr-x | MAKEALL | 16 |
1 files changed, 14 insertions, 2 deletions
@@ -802,8 +802,20 @@ build_targets() { #----------------------------------------------------------------------- kill_children() { - local pgid=`ps -p $$ --no-headers -o "%r" | tr -d ' '` - local children=`pgrep -g $pgid | grep -v $$ | grep -v $pgid` + local OS=$(uname -s) + local children="" + case "${OS}" in + "Darwin") + # Mac OS X is known to have BSD style ps + local pgid=$(ps -p $$ -o pgid | sed -e "/PGID/d") + children=$(ps -g $pgid -o pid | sed -e "/PID\|$$\|$pgid/d") + ;; + *) + # everything else tries the GNU style + local pgid=$(ps -p $$ --no-headers -o "%r" | tr -d ' ') + children=$(pgrep -g $pgid | sed -e "/$$\|$pgid/d") + ;; + esac kill $children 2> /dev/null wait $children 2> /dev/null |