> The github GUI (that is, the "Merge pull request" button) for merging pull > requests > allows 3 different options for how the merge is done. I believe the default > is "Create > a merge commit". This results in the merge commit showing up in the git log. > > I'd like to propose that we change this to "Rebase and merge", which applies > the > patches to the top of the tree. If there's agreement, or no disagreement, I > can force > this setting by disabling the other merge options.
Hearing no disagreement, I modified the git settings to use 'rebase and merge' as the merge option. This has the impact of avoiding adding merge commits into the git log. (Of course, we can always modify it back later.) - Sean _______________________________________________ ofiwg mailing list ofiwg@lists.openfabrics.org https://lists.openfabrics.org/mailman/listinfo/ofiwg
