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. - Sean _______________________________________________ ofiwg mailing list [email protected] https://lists.openfabrics.org/mailman/listinfo/ofiwg
