Marking pull requests as merged #6414
Replies: 5 comments 4 replies
-
Good example of repository with such approach is |
Beta Was this translation helpful? Give feedback.
-
Peculiar, how did those merges happen? My manual merges (with |
Beta Was this translation helpful? Give feedback.
-
Duplicates and older work on the subject:
|
Beta Was this translation helpful? Give feedback.
-
We would very much like this in FreeBSD as well. Our canonical repo is self-hosted (https://cgit.freebsd.org/src/), but we mirror to GitHub and accept contributions via pull requests to make it easy for contributors who already have GitHub accounts. We generally add a "Pull Request:" trailer for our own tracking - for example, freebsd/freebsd-src@8117ea0 which came from freebsd/freebsd-src#694. |
Beta Was this translation helpful? Give feedback.
-
I just ran into this as well with a small open source project I run that sees a few contributions once in a blue moon. This behaviour is really confusing and not having any way to tell the git UI that a PR has been manually merged is really unhelpful. I second adding a "Merges #xyz" tag. |
Beta Was this translation helpful? Give feedback.
-
Many projects do not merge PRs using GitHubs UI, for various reasons (adding sign-offs, for instance, or signing commits), and instead rely on external automation to track and close PRs after they have been applied. This marks the PRs as closed rather than merged, which has the wrong semantics (closed would imply rejected or withdrawn normally, rather than accepted).
It'd be visually useful to allow automation to mark PRs as merged, leaving closing for rejected PRs, especially of PRs can be marked as merged by a specific person.
An alternative approach could be
Merges: prnum
in commit messages. This would work for most cases I can think of off the top of my head, as merge commits already have commit messages anyway.Beta Was this translation helpful? Give feedback.
All reactions