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