I've got a GitHub repo that loosely follows git-flow. There are two long-standing branches: master and develop. Two feature branches (feature/one and feature/two) that were cut off of develop some time ago. PRs were created for both of these two merge back into develop.
The feature/one PR had junk code it in, but I accidentally merged it into develop and want to back it out. What are the specific commands I can use to "undo" this "junk PR" merge? Is it possible to do this all from inside of GitHub, or do I have to make the revert locally and then push it to GitHub?
You can still use git revert here, as you would for a non merge commit, but you'll have to also specify which parent you want to follow:
git revert <SHA-1 of merge commit> -m 1
This will add a new commit which will functionally undo the merge commit and bring the branch back to the first parent. If you wanted the second parent, you would use -m 2.
There probably is a way to directly handle this from the GitHub UI, but it can also be handled locally.