Rev 2863 | Go to most recent revision | Blame | Compare with Previous | Last modification | View Log | RSS feed
pid=`ps -a | grep trac | cut -c 1-5` if [ "$pid" != "" ] then echo "Killing process id $pid" kill $pid else echo "Trac is not running" fi
pid=`ps -a | grep trac | cut -c 1-5`
if [ "$pid" != "" ]
then
echo "Killing process id $pid"
kill $pid
else
echo "Trac is not running"
fi