michaeljb
commented
10 years ago I think github actually has some instructions next to the merge pull request option, the link says something about doing it on the command line (my internet at home went down so I'm responding by email from my phone, don't remember exactly what it says)
But anyway, I would do it slightly differently from GitHub (and this is how I have my local stuff set up):
git remote add michaeljb $michaeljb_github_url git fetch michaeljb git checkout -b jslint michaeljb/jslint
After the add remote command, your .git/config file should be updated with a few lines indicating you have a remote named "michaeljb". Note that the default remote that points to this repo is named "origin", and by default git commands like pull and push assume origin as the remote.
If you require further reading I recommend gitready.com (I think it's .com anyway) and the book "pro git", available for free in web page form.
My computer has been flaky lately and I'm half expecting it to just die soon, so I've been wanting to make sure important stuff is backed up online. Going back to using my own fork seemed better than cluttering your repo with my branches.
On Tuesday, April 29, 2014, Andrew Iannaccone notifications@github.com wrote:
I know this shouldn't be difficult, but how do i pull this branch from your repo without cloning the whole thing?
— Reply to this email directly or view it on GitHubhttps://github.com/aiannacc/Goko-Salvager/pull/210#issuecomment-41759029 .
Michael Brandt
aiannacc
I know this shouldn't be difficult, but how do i pull this branch from your repo without cloning the whole thing?