424982 improved PID check in jetty.sh

This commit is contained in:
Greg Wilkins 2014-04-25 12:56:41 +02:00
parent 8855b79be5
commit ce5af1d521
1 changed files with 15 additions and 21 deletions

View File

@ -105,8 +105,14 @@ findDirectory()
running()
{
local PID=$(cat "$1" 2>/dev/null) || return 1
kill -0 "$PID" 2>/dev/null
if [ -f "$1" ]
then
local PID=$(cat "$1" 2>/dev/null) || return 1
kill -0 "$PID" 2>/dev/null
return
fi
rm -f "$1"
return 1
}
started()
@ -408,16 +414,10 @@ case "$ACTION" in
else
if [ -f "$JETTY_PID" ]
if running $JETTY_PID
then
if running $JETTY_PID
then
echo "Already Running!"
exit 1
else
# dead pid file - remove
rm -f "$JETTY_PID"
fi
echo "Already Running $(cat $JETTY_PID)!"
exit 1
fi
if [ "$JETTY_USER" ]
@ -519,16 +519,10 @@ case "$ACTION" in
run|demo)
echo "Running Jetty: "
if [ -f "$JETTY_PID" ]
if running "$JETTY_PID"
then
if running "$JETTY_PID"
then
echo "Already Running!"
exit 1
else
# dead pid file - remove
rm -f "$JETTY_PID"
fi
echo Already Running $(cat "$JETTY_PID")!
exit 1
fi
exec "${RUN_CMD[@]}"
@ -550,7 +544,7 @@ case "$ACTION" in
echo "RUN_CMD = ${RUN_CMD[*]}"
echo
if [ -f "$JETTY_PID" ]
if running "$JETTY_PID"
then
echo "Jetty running pid=$(< "$JETTY_PID")"
exit 0