diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 55a56a2..96e2259 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -5,6 +5,10 @@ on: branches: [ master ] pull_request: branches: [ master ] + # Manual trigger. Worth having on a self-hosted runner: when a run fails for + # reasons outside the repo — the runner was down, a toolchain changed — this + # re-runs it without an empty commit to force one. + workflow_dispatch: # Both jobs target a self-hosted runner, by capability rather than by hostname. # See tool/setup_ci_runner.sh for how that runner is provisioned and why it is