[bostonvaulter2]

GitHub's merge queue does support merging multiple PRs in a single merge operation. It's the "Maximum pull requests to merge" setting