Hello, GitHub proposes these commands to merge a pull requests (explanations from me, to make sure I got it correctly)
# Basically branch develop to davidsblom-develop git checkout -b davidsblom-develop develop # Pull in foreign repos commits from foreign develop branch. git pull git://github.com/davidsblom/precice.git develop # Edit and merge the changes to the main repos develop branch git checkout develop git merge --no-ff davidsblom-develop git push origin develop My question is, if davidsblom make further commits to his develop branch (after the pull request was issued) aren't these commits also included in the pull and therefore in the merge? If yes, isn't the idea to merge just the changes that the pull request was about? If not, why? ;-) Thanks, Florian -- To unsubscribe from this list: send the line "unsubscribe git" in the body of a message to majord...@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html
