diff options
Diffstat (limited to 'dev-db/monetdb/files/monetdb-stop.sh')
| -rw-r--r-- | dev-db/monetdb/files/monetdb-stop.sh | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/dev-db/monetdb/files/monetdb-stop.sh b/dev-db/monetdb/files/monetdb-stop.sh deleted file mode 100644 index aa562e814f98..000000000000 --- a/dev-db/monetdb/files/monetdb-stop.sh +++ /dev/null @@ -1,26 +0,0 @@ -#! /bin/sh - -LOG=/var/log/monetdb/Mserver.log -if [ -f ~monetdb/Mserver.pid ]; then - MPID=`cat ~monetdb/Mserver.pid` -else - echo "No Mserver PID found" - exit -1 -fi - -echo `date` Stopping MonetDB \(PID: $MPID\) >> $LOG -kill -TERM $MPID || exit -1 -sleep 1 -ALIVE=`ps --no-heading --format pid -p $MPID` -if [ "$ALIVE" = "$MPID" ]; then - echo Mserver still alive after TERM, trying KILL... >> $LOG - kill -KILL $MPID - sleep 2 - ALIVE=`ps --no-heading --format pid -p $MPID` - if [ "$ALIVE" = "$MPID" ]; then - echo "Failed to stop process $MPID" - exit -1 - fi -fi -echo `date` Mserver stopped >> $LOG -rm -f ~monetdb/Mserver.pid > /dev/null |