File size: 309 Bytes
42b02cd | 1 2 3 4 5 6 7 8 9 10 11 12 | #!/usr/bin/env bash
set -euo pipefail
ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
PID_FILE="$ROOT/runtime/server.pid"
[[ -f "$PID_FILE" ]] || { echo 'No PID file.'; exit 0; }
PID="$(cat "$PID_FILE")"
if kill -0 "$PID" 2>/dev/null; then
kill "$PID"
echo "Stopped PID $PID"
fi
rm -f "$PID_FILE"
|