Thank you!


 
git remote add upstream git@github.com:TEIC/TEI.git (if you haven’t already done this)
git pull upstream dev

ought to do the trick.

I have on my local HD a copy of a fork one of our repos.[1] The interesting bit of this repo is in its dev branch. But sadly, its dev branch is somewhat behind our dev branch. So I would like to merge our dev branch in. How do I do that? I.e., how do I specify that I want the git merge​ command to use our repo’s dev branch (not the current repo’s dev branch, which would be silly, as I am on the current repo’s dev branch) as the upstream?

Note
[1] https://github.com/sanskrit-coders/Stylesheets.git to be precise, but that detail does not matte