Prepare github actions pipelines for merge queue (#7315)

Github has a built in merge queue. I think it would be good to try this
out, to speed up merging PRs when multiple people want to merge at the
same time. This PR does not enable it yet, but it starts triggering
Github actions also for the `merge_queue` event. This is a requirement
for trying them out.

Announcment:
https://github.blog/2023-07-12-github-merge-queue-is-generally-available/
Docs:
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue
pg16_grant_inherit_set
Jelte Fennema-Nio 2023-11-02 09:23:34 +01:00 committed by francisjodi
parent b2338b1a6c
commit 22c8c17f70
2 changed files with 2 additions and 0 deletions

View File

@ -16,6 +16,7 @@ on:
- "release-*"
pull_request:
types: [opened, reopened,synchronize]
merge_group:
jobs:
# Since GHA does not interpolate env varibles in matrix context, we need to
# define them in a separate job and use them in other jobs.

View File

@ -3,6 +3,7 @@ name: Build tests in packaging images
on:
pull_request:
types: [opened, reopened,synchronize]
merge_group:
workflow_dispatch: