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.

On Mar 23, 2021, at 12:59, Bauman, Syd <s.bauman@northeastern.edu> wrote:


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 matter.
_______________________________________________
Tei-council mailing list
Tei-council@lists.tei-c.org
http://lists.lists.tei-c.org/mailman/listinfo/tei-council