On Thu, Dec 1, 2016 at 4:25 PM, Gilles Gouaillardet <gil...@rist.or.jp> wrote: [...]
> git checkout master > > git merge --ff-only topic/misc_fixes > > git push origin master > [...] Gilles, 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 -- 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 devel@lists.open-mpi.org https://rfd.newmexicoconsortium.org/mailman/listinfo/devel
