ci: trigger on merge_group for GitHub merge queue #139

Merged
JMR-dev merged 1 commits from ci-merge-queue-trigger into main 2026-07-02 15:21:53 +00:00
+4
View File
@@ -4,6 +4,10 @@ name: CI
on:
pull_request:
branches: [main]
# Run the same jobs when a PR is queued in the GitHub merge queue, so the "CI passed"
# gate reports on the up-to-date merge-group ref and the queue can merge in order.
merge_group:
branches: [main]
# A new push to a PR cancels any in-flight run for that PR.
concurrency: