Skip to content

Commit

Permalink
chore(ci): allow GitHub merge queue (#298)
Browse files Browse the repository at this point in the history
this commit adds `merge_group` to the CI workflow, so that we can
eventually enable GitHub's merge queue.
  • Loading branch information
hawkw committed Oct 26, 2023
1 parent b3b4da9 commit 29174ad
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
@@ -3,10 +3,14 @@
name: CI

on:
# always run CI on pushes to PRs and to the `main` branch
pull_request:
workflow_dispatch:
push:
branches: ["main"]
# allow manually triggering CI.
workflow_dispatch:
# enable merge queue.
merge_group:

env:
# disable incremental compilation.

0 comments on commit 29174ad

Please sign in to comment.