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.