From efa183b54f02fdd5666312792fc73552b6f06ec6 Mon Sep 17 00:00:00 2001
From: Faiyaz Ahmed <faiyaza@cs.princeton.edu>
Date: Wed, 19 Mar 2008 19:54:50 +0000
Subject: [PATCH] Must use vkill to kill outside of root.

---
 pl_mop.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pl_mop.sh b/pl_mop.sh
index 0a512c0..97dad39 100755
--- a/pl_mop.sh
+++ b/pl_mop.sh
@@ -206,7 +206,7 @@ kill_nm_inslice(){
         line=$(vps aux | grep $pid)
         echo NM found in slice. Killing PID $pid
         echo $line
-        kill -9 $pid
+        vkill -9 $pid
     done
 }
 
-- 
2.43.0