On Thu, Dec 1, 2016 at 4:25 PM, Gilles Gouaillardet <gil...@rist.or.jp>
> git checkout master
> git merge --ff-only topic/misc_fixes
> git push origin master
You characterized the merge commit has having "close to zero added value"
to you - but in this instance it would have saved you and others a
non-trivial amount of time in email.
Additionally, in projects I work on we value that merge commit as a "cut
line" if we ever need to revert an entire PR for some reason. Using
git-bisect such that one includes or excludes the entire PR is also a
justification for keeping the merge commit. So my opinion is that you
should have omitted "--ff-only" and entered a commit message that at least
identified the PR number.
> though this does not generate a git commit, github.com is smart enough to
> figure this out and marks the PR as merged.
FWIW: "smart enough" is simply a detection that the last commit in the PR
has become an ancestor of the current HEAD.
Paul H. Hargrove phhargr...@lbl.gov
Computer Languages & Systems Software (CLaSS) Group
Computer Science Department Tel: +1-510-495-2352
Lawrence Berkeley National Laboratory Fax: +1-510-486-6900
devel mailing list