16 lines
443 B
Bash
Executable File
16 lines
443 B
Bash
Executable File
#!/usr/bin/env bash
|
|
# Restarts the dsh web server: kills the running `dsh web` first, then starts a fresh one.
|
|
set -euo pipefail
|
|
|
|
pids="$(pgrep -f "dsh web" 2>/dev/null || true)"
|
|
if [[ -n "$pids" ]]; then
|
|
echo "killing existing dsh web (pid: $(echo "$pids" | tr '\n' ' '))"
|
|
echo "$pids" | xargs kill 2>/dev/null || true
|
|
for _ in {1..50}; do
|
|
pgrep -f "dsh web" >/dev/null 2>&1 || break
|
|
sleep 0.1
|
|
done
|
|
fi
|
|
|
|
exec dsh web --no-open
|