Externally merged commits are not marked as merged #13181

Closed
opened 2025-11-02 10:33:51 -06:00 by GiteaMirror · 11 comments
Owner

Originally created by @AdamMajer on GitHub (Jun 20, 2024).

Description

  1. create repo
  2. create fork
  3. do channge and create PR to repo
  4. merge manually with git merge --ff-only ... as per instructions
  5. PR not marked as merged, just says the commit already there and nothing to do.

Gitea Version

1.22 , or demo site

Can you reproduce the bug on the Gitea demo site?

Yes

Log Gist

No response

Screenshots

from: https://demo.gitea.com/gnuman/test/pulls/1

image

THEN I added another commit, and it got added to the PR (I guess since it wasn't closed) and the instructions are different from above. Maybe above it reverted to default ones? But this could be another issue not related to this one.

image

Git Version

No response

Operating System

No response

How are you running Gitea?

demo site

Database

None

Originally created by @AdamMajer on GitHub (Jun 20, 2024). ### Description 1. create repo 2. create fork 3. do channge and create PR to repo 4. merge manually with `git merge --ff-only ...` as per instructions 5. PR not marked as merged, just says the commit already there and nothing to do. ### Gitea Version 1.22 , or demo site ### Can you reproduce the bug on the Gitea demo site? Yes ### Log Gist _No response_ ### Screenshots from: https://demo.gitea.com/gnuman/test/pulls/1 > ![image](https://github.com/go-gitea/gitea/assets/1211498/79ce2ed8-0057-4071-9b33-67f25813bcb0) **THEN** I added another commit, and it got added to the PR (I guess since it wasn't closed) and the instructions are different from above. Maybe above it reverted to default ones? But this could be another issue not related to this one. > ![image](https://github.com/go-gitea/gitea/assets/1211498/0e577e67-f19d-4fac-b8d1-b58eb59bdd13) ### Git Version _No response_ ### Operating System _No response_ ### How are you running Gitea? demo site ### Database None
GiteaMirror added the type/bug label 2025-11-02 10:33:51 -06:00
Author
Owner

@wxiaoguang commented on GitHub (Jun 20, 2024):

Workaround: you could enable "Manually Merge" in the repo settings, and manually merge it.


ps: not sure whether it is a regression, I never used that workflow 🤔 is there any further information to confirm whether it is a regression?

@wxiaoguang commented on GitHub (Jun 20, 2024): Workaround: you could enable "Manually Merge" in the repo settings, and manually merge it. ---- ps: not sure whether it is a regression, I never used that workflow 🤔 is there any further information to confirm whether it is a regression?
Author
Owner

@AdamMajer commented on GitHub (Jun 20, 2024):

Manual merge is a workaround, I think.

If I'm following the command-line instructions, gitea should be smart enough to notice that the commits are there in the branch already, and close it as merged. The logic is simply, on push to target branch, if "all commits exist in the target branch, so it's merged, mark as done".

Is there a common use-case when this is not desired?

@AdamMajer commented on GitHub (Jun 20, 2024): Manual merge is a workaround, I think. If I'm following the command-line instructions, gitea should be smart enough to notice that the commits are there in the branch already, and close it as merged. The logic is simply, on push to target branch, if "all commits exist in the target branch, so it's merged, mark as done". Is there a common use-case when this is not desired?
Author
Owner

@AdamMajer commented on GitHub (Jun 20, 2024):

You are correct, maybe this is not a regression. It just maybe never worked.

@AdamMajer commented on GitHub (Jun 20, 2024): You are correct, maybe this is not a regression. It just maybe never worked.
Author
Owner

@delvh commented on GitHub (Jun 20, 2024):

Is there a common use-case when this is not desired?

performance. And no one implemented it so far.
But I do think it is non-trivial to find all PRs that can be closed once you push:
You need to find all PRs that target the branch you push to.
On top of that, you then need to ensure that all commits are contained within your branch - the only way to do this reliably is by asking Git on every matching PR individually if there are diverging commits.
You cannot just do a DB lookup as then the case you merged the branch locally and added a commit on top before pushing is not covered (although that is a rare edge case)

The moment you have a repo with lots of open PRs, I can predict that pushing will take forever, especially if your hardware isn't the strongest.
However, the performance problem could be solved by adding a instance-wide setting that toggles this behavior.

@delvh commented on GitHub (Jun 20, 2024): > Is there a common use-case when this is not desired? performance. And no one implemented it so far. But I do think it is non-trivial to find all PRs that can be closed once you push: You need to find all PRs that target the branch you push to. On top of that, you then need to ensure that all commits are contained within your branch - the only way to do this reliably is by asking Git on every matching PR individually if there are diverging commits. You cannot just do a DB lookup as then the case `you merged the branch locally and added a commit on top before pushing` is not covered (although that is a rare edge case) The moment you have a repo with lots of open PRs, I can predict that pushing will take forever, especially if your hardware isn't the strongest. However, the performance problem could be solved by adding a instance-wide setting that toggles this behavior.
Author
Owner

@AdamMajer commented on GitHub (Jun 21, 2024):

Well, you only need to check the if the commit id of PR head is in the target branch, nothing else.. If that is the case, then it's merged. IFF the PR head commit id is in the branch head, then the PR is FF merged.

You cannot just do a DB lookup as then the case you merged the branch locally and added a commit on top before pushing is not covered (although that is a rare edge case)

As long as the commit id from PR head is there, it has to be merged. Other things on-top, well, maybe extra commits? But that is a different discussion, I think.

What has to be done is, for all pushes to target repo, check all open PR if the commit id is in the repo, if yes, mark as merged. Nothing more to do.

If no one does this, I'll try to get to it next week.

@AdamMajer commented on GitHub (Jun 21, 2024): Well, you only need to check the if the commit id of PR head is in the target branch, nothing else.. If that is the case, then it's merged. IFF the PR head commit id is in the branch head, then the PR is FF merged. > You cannot just do a DB lookup as then the case you merged the branch locally and added a commit on top before pushing is not covered (although that is a rare edge case) As long as the commit id from PR head is there, it has to be merged. Other things on-top, well, maybe extra commits? But that is a different discussion, I think. What has to be done is, for all pushes to target repo, check all open PR if the commit id is in the repo, if yes, mark as merged. Nothing more to do. If no one does this, I'll try to get to it next week.
Author
Owner

@delvh commented on GitHub (Jun 21, 2024):

Well, you only need to check the if the commit id of PR head is in the target branch, nothing else.

Yes, but you first need to find all applicable PRs and do this git call for all of them separately, so that point still stands.
But sure, go ahead, I'll review your PR dutifully once it exists.
(If I forget to, ping me. Unfortunately, my TODO list is so long that I frequently forget what I wanted to do)

@delvh commented on GitHub (Jun 21, 2024): > Well, you only need to check the if the commit id of PR head is in the target branch, nothing else. Yes, but you first need to find all applicable PRs and do this git call for all of them separately, so that point still stands. But sure, go ahead, I'll review your PR dutifully once it exists. (If I forget to, ping me. Unfortunately, my TODO list is so long that I frequently forget what I wanted to do)
Author
Owner

@a1012112796 commented on GitHub (Aug 8, 2024):

I has try a new solution in https://github.com/go-gitea/gitea/pull/21951 . which try add a new push option to notify server that a pull request was merged in this push operation (example git push -o pulls.merged=1,2,3 -u origin master). I think it would be a better way.

@a1012112796 commented on GitHub (Aug 8, 2024): I has try a new solution in https://github.com/go-gitea/gitea/pull/21951 . which try add a new push option to notify server that a pull request was merged in this push operation (example `git push -o pulls.merged=1,2,3 -u origin master`). I think it would be a better way.
Author
Owner

@a1012112796 commented on GitHub (Aug 8, 2024):

if "all commits exist in the target branch, so it's merged, mark as done".
? Is there a common use-case when this is not desired?

Because empty pull request has been allowed in https://github.com/go-gitea/gitea/pull/12543

@a1012112796 commented on GitHub (Aug 8, 2024): > if "all commits exist in the target branch, so it's merged, mark as done". > ? Is there a common use-case when this is not desired? Because empty pull request has been allowed in https://github.com/go-gitea/gitea/pull/12543
Author
Owner

@AdamMajer commented on GitHub (Aug 8, 2024):

Well, the idea here is if a PR head commit ID is present in the new push to the target branch, then it's merged. Nothing else needed.

This of course will not detect anything when the commit is altered in any way because then the commit ID will be changed. Another solution would then be required for those workflows. The push option looks like it would be helpful in those cases.

@AdamMajer commented on GitHub (Aug 8, 2024): Well, the idea here is if a PR head commit ID is present in the new push to the target branch, then it's merged. Nothing else needed. This of course will not detect anything when the commit is altered in any way because then the commit ID will be changed. Another solution would then be required for those workflows. The push option looks like it would be helpful in those cases.
Author
Owner

@AdamMajer commented on GitHub (Aug 8, 2024):

I don't quite understand the point of empty PR. It seems they would just be issues. But empty PR are not the same as a PR with a HEAD commit ID present in a push to target branch. Or am I misunderstanding this?

@AdamMajer commented on GitHub (Aug 8, 2024): I don't quite understand the point of empty PR. It seems they would just be issues. But empty PR are not the same as a PR with a HEAD commit ID present in a push to target branch. Or am I misunderstanding this?
Author
Owner

@AdamMajer commented on GitHub (May 19, 2025):

I'll close this now as autodetected manual merge feature does the job here.

@AdamMajer commented on GitHub (May 19, 2025): I'll close this now as autodetected manual merge feature does the job here.
Sign in to join this conversation.
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: github-starred/gitea#13181