chore: add support to merge queues (#1192)

This change is necessary before enabling merge queues. The `merge_group`
event is needed to trigger the GitHub Actions workflow when a pull
request is added to a merge queue.

The merge queue provides the same benefits as the Require branches to be
up to date before merging branch protection but does not require a pull
request author to update their pull request branch and wait for status
checks to finish before trying to merge. More info on
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue.
This commit is contained in:
diegomrsantos 2024-09-10 18:10:24 +02:00 committed by GitHub
parent 1771534030
commit 3e3df07269
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 4 additions and 0 deletions

View File

@ -5,6 +5,7 @@ on:
branches: branches:
- master - master
pull_request: pull_request:
merge_group:
workflow_dispatch: workflow_dispatch:
concurrency: concurrency:

View File

@ -6,6 +6,7 @@ on:
branches: branches:
- master - master
pull_request: pull_request:
merge_group:
workflow_dispatch: workflow_dispatch:
concurrency: concurrency:

View File

@ -2,6 +2,7 @@ name: Interoperability Tests
on: on:
pull_request: pull_request:
merge_group:
push: push:
branches: branches:
- master - master

View File

@ -2,6 +2,7 @@ name: Linters
on: on:
pull_request: pull_request:
merge_group:
concurrency: concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}