Re:GitHub is down
by NikkiA on Monday July 22, 2019 @08:54PM
(#20503596)
Merge the PR on github, pull to your local copy (now you're ahead of one of the urls of origin), push (and it should just push to the origin that's behind)
If you have any discrepencies in between them, you'll need to merge locally of course.
If you have any discrepencies in between them, you'll need to merge locally of course.