Empty pull request from fork's main to main flagges as "auto merged"

[koppor]

Select Topic Area

Question

Body

1. Pull Request Fix inserting new entry JabRef/jabref#12123 was merged into main
2. Merge queue is activated, thus following output
   
3. Pull Request Display cover image as SplitPane JabRef/jabref#12108 is from main branch.
4. Pull Request Display cover image as SplitPane JabRef/jabref#12108 has 0 commits
5. Pull Request Display cover image as SplitPane JabRef/jabref#12108 was flagged as merged on the same time as merge of step 2:
   

We are getting nervous at step 5: Can anyone merge content into our main branch if their pull requests originates from main?

I think, the answer is "no", but I would like to have this clarified:

Wish: GitHub should not close pull requests with 0 commits if another pull requests is merged using the merge queue.

[ghostinhershell]

Hi @koppor, thanks so much for reaching out in our community 👋🏾

We are getting nervous at step 5: Can anyone merge content into our main branch if their pull requests originates from main?
The answer to this question depends on the access level of your repo (is it private or public?) and the access levels for your collaborators. See: https://docs.github.com/en/issues/planning-and-tracking-with-projects/managing-your-project/managing-access-to-your-projects.

From the screenshot, it looks like these branches were automated to be merged as part of a merge queue:

Once a pull request has passed all required branch protection checks, a user with write access to the repository can add the pull request to the queue. The merge queue will ensure the pull request's changes pass all required status checks when applied to the latest version of the target branch and any pull requests already in the queue.

Reference: https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/incorporating-changes-from-a-pull-request/merging-a-pull-request-with-a-merge-queue#adding-a-pull-request-to-a-merge-queue

Does that clarify things a bit?