Jelte Fennema-Nio ea5551689e 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		2023-11-02 08:23:34 +00:00
..
build_and_test.yml	Prepare github actions pipelines for merge queue (#7315)	2023-11-02 08:23:34 +00:00
codeql.yml	Create CodeQL workflow for static analysis (#5868)	2023-02-07 15:25:17 +03:00
devcontainer.yml	Add devcontainer for development purposes (#7102)	2023-10-09 15:37:21 +02:00
flaky_test_debugging.yml	Removes use-base-schedule flag from CI (#7301)	2023-11-01 15:52:22 +00:00
packaging-test-pipelines.yml	Prepare github actions pipelines for merge queue (#7315)	2023-11-02 08:23:34 +00:00