Prepare github actions pipelines for merge queue

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
pull/7315/head
Jelte Fennema-Nio 2023-11-01 18:35:57 +01:00
parent 5903196020
commit f3bc1a6676
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_queue:
workflow_dispatch: