#2969 Manually merging a PR / declare empty PRs to be successfully merged
Closed: Duplicate Opened by thm.

After manually merging a pull request (git merge origin/pull/1), pagure correctly notices that the patch now is empty. Nevertheless, I cannot "successfully" close the PR. All I can do, is hit the red X ("close the PR without merging it"), but that yields to a red box on the PR stating that I closed it.

There should be an option "successfully" close empty PRs, aka declare them to be merged.


You can do this by modifying the commit you're merging locally and add a "Merge in its message.

That will close the PR when you push (if you have the pagure hook enabled in the settings).

The alternative asking pagure to do it automatically has been requested in https://pagure.io/pagure/issue/1683

So I'm going to close this ticket as duplicate.

Thanks for filling it though, it's always appreciated!

Metadata Update from @pingou:
- Issue close_status updated to: Duplicate

You can do this by modifying the commit you're merging locally and add a "Merge in its message.
That will close the PR when you push (if you have the pagure hook enabled in the settings).

Which would mean I cannot FF, but need to create a merge commit, right?

No you can fast-forward, you just need to git am the patch, git commit --amend to add that line to the commit message and then you can git push.

Metadata