GitHub Pull Request merge commands

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.c

Right way to import a repo

Hello, I have two repositories. tools and flof. I want to merge flof into tools (and flof will be deleted after that) while keeping history intact. Of course I've googled that and found a number of different solution which all seem to be pretty komplex, so I just tried it myself. It seems to wo