diegomrsantos 3e3df07269 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.		2024-09-10 16:10:24 +00:00
..
actions/install_nim	chore: Cleanup CI (#1117)	2024-08-06 16:24:13 +02:00
workflows	chore: add support to merge queues (#1192)	2024-09-10 16:10:24 +00:00