From d07e652fd9ef593dea6fd0052f7ffc2338643d5c Mon Sep 17 00:00:00 2001 From: Eliza Weisman Date: Tue, 10 Oct 2023 09:15:20 -0700 Subject: [PATCH] chore: add `merge_group` trigger to CI This will allow us to use the GitHub Actions merge queue, which is a bit nicer for merging multiple PRs while ensuring that they are up to date with the latest base branch. --- .github/workflows/CI.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index a672bb28..ac93e0c1 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -4,7 +4,8 @@ on: push: branches: - master - pull_request: {} + pull_request: + merge_group: env: # Disable incremental compilation.