From e6df143aac5d163b7afd32d1112cfc5cc9c6473b Mon Sep 17 00:00:00 2001 From: Jay McCarthy Date: Tue, 4 May 2010 12:04:10 -0600 Subject: [PATCH] New program names --- collects/meta/drdr/good-init.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/meta/drdr/good-init.sh b/collects/meta/drdr/good-init.sh index 833be414f6..ed6c58f745 100755 --- a/collects/meta/drdr/good-init.sh +++ b/collects/meta/drdr/good-init.sh @@ -9,7 +9,7 @@ cd "$DRDR" kill_all() { cat "$LOGS/"*.pid > /tmp/leave-pids-$$ - KILL=`pgrep '^(Xvfb|fluxbox|mzscheme|mred(-text)?)$' | grep -w -v -f /tmp/leave-pids-$$` + KILL=`pgrep '^(Xvfb|fluxbox|racket|gracket(-text)?)$' | grep -w -v -f /tmp/leave-pids-$$` rm /tmp/leave-pids-$$ kill -15 $KILL sleep 2