diff --git a/openbis/dist/server/shutdown.sh b/openbis/dist/server/shutdown.sh index 225a5c9effe13b1bac42bee28ef10a51663f3312..180568a41ab8844add38a61712a265d249439437 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