git/list[1] front-page[2] threads[3] people[4] search[5] about
 

GitHub Pull Request merge commands

From
FLFlorian Lindner <mailinglists@xgm.de>
Date
Jun 16, 2015, 08:55 UTC
Message-ID
<mloo9l$agl$6@ger.gmane.org>
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

Next: Johannes Löthberg
Message 1 of 2 in “GitHub Pull Request merge commands”
  1. Florian LindnerJun 16, 2015
  2. Johannes LöthbergJun 16, 2015

Read the whole thread, see it on lore, or plain text.

$ cat FOOTERMessages come from the public archive at lore.kernel.org/git, fetched every hour. The front page is chosen and written each morning by an AI editor and can be wrong; the threads themselves are the record. About and API. For agents: an MCP server at https://gitlist.dev/mcp, and any thread, story or person page as Markdown by adding .md to its URL (or sending Accept: text/markdown). Details in /llms.txt.