43 lines
1.0 KiB
Bash
43 lines
1.0 KiB
Bash
#!/usr/bin/env bash
|
|
set -euo pipefail
|
|
|
|
ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
|
|
cd "$ROOT_DIR"
|
|
|
|
EDGE_RUNTIME_DIR="${EDGE_RUNTIME_DIR:-runtime}"
|
|
PID_DIR="${EDGE_RUNTIME_DIR}/pids"
|
|
WORKER_PID_FILE="${PID_DIR}/worker.pid"
|
|
EDGE_CLIENT_PID_FILE="${PID_DIR}/edge_client.pid"
|
|
|
|
stop_by_pid_file() {
|
|
local name="$1"
|
|
local pid_file="$2"
|
|
if [ ! -f "$pid_file" ]; then
|
|
echo "[INFO] ${name} not running (no pid file)"
|
|
return
|
|
fi
|
|
|
|
local pid
|
|
pid="$(cat "$pid_file" 2>/dev/null || true)"
|
|
if [ -z "$pid" ]; then
|
|
rm -f "$pid_file"
|
|
echo "[INFO] ${name} pid file empty, cleaned"
|
|
return
|
|
fi
|
|
|
|
if kill -0 "$pid" >/dev/null 2>&1; then
|
|
kill "$pid" >/dev/null 2>&1 || true
|
|
sleep 1
|
|
if kill -0 "$pid" >/dev/null 2>&1; then
|
|
kill -9 "$pid" >/dev/null 2>&1 || true
|
|
fi
|
|
echo "[OK] ${name} stopped (pid ${pid})"
|
|
else
|
|
echo "[INFO] ${name} already stopped (stale pid ${pid})"
|
|
fi
|
|
rm -f "$pid_file"
|
|
}
|
|
|
|
stop_by_pid_file "edge client" "$EDGE_CLIENT_PID_FILE"
|
|
stop_by_pid_file "worker" "$WORKER_PID_FILE"
|