From 29174ad9f8665996a37f8d6bd5d74c3ce3d570ad Mon Sep 17 00:00:00 2001 From: Eliza Weisman Date: Thu, 26 Oct 2023 09:52:34 -0700 Subject: [PATCH] chore(ci): allow GitHub merge queue (#298) this commit adds `merge_group` to the CI workflow, so that we can eventually enable GitHub's merge queue. --- .github/workflows/ci.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8ed7bd54..86776efa 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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.