#!/bin/sh if [ "X$ARB_PID" = "X" ] ; then pidfiles=/tmp/arb_pids_$USER_* if [ "X$pidfiles" = "X" ]; then exit 0; fi else pidfiles=/tmp/arb_pids_${USER}_${ARB_PID} fi if [ "\"X$pidfiles\"" != "X" ]; then kill -9 `cat $pidfiles` >/dev/null 2>&1 rm -f $pidfiles fi rm -f /tmp/arb_*_${USER}_${ARB_PID}*