-
Notifications
You must be signed in to change notification settings - Fork 691
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merge pull-requests by commit disabled? #280
Comments
I don't remember exactly, but this was probably me. Why do we want this enabled, though? We never use that functionality as it makes a sloppy git history. Our policy is:
|
The citation primarily refers to single commits and fixup commits, which indeed should not clutter the git history. Merge-commits make a lot of sense if there are multiple, clearly distinguishable commits in a single PR! |
Often that's a viable option, yes. However, rebase-merging also disguises the extension of a merge (you don't see the start and end of the related commits anymore) and the PR id is not reported by github. |
I'm not aware of an agreement to never use merge commits in moveit and neither Robert nor I seem to agree.
one of git's design goals are short-living feature branches that can be merged. |
Sounds good, I've re-enabled merging. Can you copy that policy your wrote out on our Pull Request page please? You can just edit on Github: |
I just wanted to merge #278 and found the
Create a merge commit
field disabled:@davetcoleman @mlautman @rhaschke Did someone disable this option?
I guess it is still possible to do this by hand in git, right?
It's not a big deal for this request, but in general I would prefer to have this possibility.
The text was updated successfully, but these errors were encountered: