From a6fc965f9305ac7eaae343958e4ee8a0ab07ddce Mon Sep 17 00:00:00 2001
From: brinn <brinn>
Date: Sun, 2 Sep 2012 19:01:02 +0000
Subject: [PATCH] Ensure we delete the PID file only if the process died.
SVN: 26504
---
openbis/dist/server/shutdown.sh | 23 ++++++++++++++++++++++-
1 file changed, 22 insertions(+), 1 deletion(-)
diff --git a/openbis/dist/server/shutdown.sh b/openbis/dist/server/shutdown.sh
index 225a5c9effe..180568a41ab 100755
--- a/openbis/dist/server/shutdown.sh
+++ b/openbis/dist/server/shutdown.sh
@@ -11,4 +11,25 @@ $JVM -DSTOP.PORT=$JETTY_STOP_PORT \
-jar start.jar --stop
# Delete PID file
-test -f "$JETTY_PID_FILE" && rm -f "$JETTY_PID_FILE"
\ No newline at end of file
+if [ -f "$JETTY_PID_FILE" ]; then
+ PID=`cat $JETTY_PID_FILE`
+ count=0
+ while [ 1 ]; do
+ isPIDRunning $PID
+ if [ $? -ne 0 ]; then
+ break
+ fi
+ count=$(($count+1))
+ if [ $count -eq 10 ]; then
+ break
+ fi
+ sleep 1
+ done
+
+ isPIDRunning $PID
+ if [ $? -ne 0 ]; then
+ rm -f "$JETTY_PID_FILE"
+ else
+ echo "Failed to shutdown PID $PID." > /dev/stderr
+ fi
+fi
\ No newline at end of file
--
GitLab