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