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?

[koppor]

I do not understand why a merge-queue of one pull request closes a completely different pull request.

As screenshots - one commit closed TWO DIFFERENT pull requests.

I also did not find it in the documentation. The linked documentation does not state something about the created commits.

---

In other words:

GitHub references a commit in the message:

This is following commit:

But the PR linked is JabRef/jabref#12123

Either the commit message should reference TWO PRs - or the second PR should not be closed with that commit. (Due to consisentcy reasons)

[github-actions[bot]]

🕒 Discussion Activity Reminder 🕒

This Discussion has been labeled as dormant by an automated system for having no activity in the last 60 days. Please consider one the following actions:

1️⃣ Close as Out of Date: If the topic is no longer relevant, close the Discussion as out of date at the bottom of the page.

2️⃣ Provide More Information: Share additional details or context — or let the community know if you've found a solution on your own.

3️⃣ Mark a Reply as Answer: If your question has been answered by a reply, mark the most helpful reply as the solution.

Note: This dormant notification will only apply to Discussions with the Question label. To learn more, see our recent announcement.

Thank you for helping bring this Discussion to a resolution! 💬