| 12345678910111213141516171819202122 |
- #!/usr/bin/env bash
- set -euo pipefail
- SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
- cd "$SCRIPT_DIR"
- PID_FILE="server.pid"
- if [[ ! -f "$PID_FILE" ]]; then
- echo "No PID file found; server not running?"
- exit 1
- fi
- PID=$(cat "$PID_FILE")
- if kill -0 "$PID" >/dev/null 2>&1; then
- kill "$PID"
- sleep 1
- echo "Server (PID $PID) terminated."
- else
- echo "PID $PID is not running."
- fi
- rm -f "$PID_FILE"
|
