If you merge a PR into github, please use "Rebase and merge" instead of "Create a merge commit". The former makes git log cleaner and easier to find specific commits to cherry-pick.
You can change the merge setting by clicking on the down arrow next to the merge button. - Sean _______________________________________________ ofiwg mailing list [email protected] https://lists.openfabrics.org/mailman/listinfo/ofiwg
