diff --git a/util/m b/util/m index f3b8ce55ce3ae92a9e170a52cddbf8201e41c404..06900fcab4e9999918647c1572f64fe9296d8a04 100755 --- a/util/m +++ b/util/m @@ -9,7 +9,7 @@ else host=$1 fi -pid=`ps ax | grep "mininet:$host$" | grep bash | awk '{print $1};'` +pid=`ps ax | grep "mininet:$host$" | grep bash | grep -v mnexec | awk '{print $1};'` if echo $pid | grep -q ' '; then echo "Error: found multiple mininet:$host processes"