How to modify a github PR that isn't mine

GitHub now allows people with write access to a repo to modify PRs that don't belong to them:


Checking out pull requests locally