diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9ff7d43..7401f9e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -4,6 +4,8 @@ on: pull_request: push: branches: [master] + # Allow maintainers to manually kick CI when GitHub doesn't create a run for a new head SHA. + workflow_dispatch: concurrency: group: ci-${{ github.workflow }}-${{ github.ref }}