threads / discuss / 39642

GitHub Pull Request merge commands

Subject: GitHub Pull Request merge commands

## tl;dr

2 messages between Jun 16, 2015 and Jun 16, 2015.

replies: 1people: 2as markdown or json

Florian Lindner· Jun 16, 2015, 08:55 UTC · lore

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

Johannes Löthberg· Jun 16, 2015, 09:33 UTC · re: Florian Lindner · lore

Re: GitHub Pull Request merge commands

On 16/06, Florian Lindner wrote:

Show 5 quoted lines

>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? ;-)
>

A pull request is "about" all commits in the branch, which is why topic-branches should be used for PRs.

-- 
Sincerely,
  Johannes Löthberg
  PGP Key ID: 0x50FB9B273A9D0BB5
  https://theos.kyriasis.com/~kyrias/