Closed
Description
We require pull requests to be up-to-date before merging. This ensures that all tests and reference files are fresh and we do not accidentally commit a breaking change. However, with recent activity this setup is becoming annoying because one has to manually keep their pull request up-to-date. Instead, we could implement merge queues:
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue