| # scripts/launch_after.sh | |
| # | |
| # Wait for a PID to exit, then fire a launcher script. Designed to be | |
| # itself run detached under nohup, so an SSH disconnect during the wait | |
| # doesn't stop the watcher. | |
| # | |
| # Usage: | |
| # nohup bash scripts/launch_after.sh <pid> <launcher.sh> [args...] \ | |
| # > logs/install/<stamp>_watcher/wait.log 2>&1 & | |
| # | |
| # Or via the helper: | |
| # bash scripts/launch_after_detached.sh <pid> <launcher.sh> [args...] | |
| set -euo pipefail | |
| ROOT="$(cd "$(dirname "$0")/.." && pwd)" | |
| cd "${ROOT}" | |
| if [[ $# -lt 2 ]]; then | |
| echo "usage: $0 <pid> <launcher.sh> [args...]" >&2 | |
| exit 2 | |
| fi | |
| PID="$1"; shift | |
| LAUNCHER="$1"; shift | |
| echo "[$(date -u +%FT%TZ)] watching PID ${PID}; will fire ${LAUNCHER} $* when it ends" | |
| while kill -0 "${PID}" 2>/dev/null; do sleep 30; done | |
| echo "[$(date -u +%FT%TZ)] PID ${PID} exited; firing ${LAUNCHER}" | |
| exec bash "${LAUNCHER}" "$@" | |