Received a pull-request from someone else, how to edit it before merging directly on github?

Question

(For reference, here is a command line git solution How to handle review a pull-request, modify code, and merge?)

Here I'm looking for a 100% in-browser solution directly in the Github interface.

• I have a repo foobar
• I receive a pull request from user bob
• I would like to make a few tiny edits on his modifications, and merge this PR

How to do this 100% from the Github interface, without having to open a command-line and do git ... operations?

Note: I don't want to merge bob's as it is, and do modifications later in a further commit. I would like to edit his PR before merging it to my project.

Erotica

Answer 1

First go in the Files changed tab of the pull request. There you could edit the files with the Edit file button.

That works if you have write access to the repo and the pull request author enables Allow edits by maintainers. (Enabled by default)

The checkbox could also be checked or unchecked after creating the pull request.

Inconsolable

Thanks @Julian! Can I ask someone who made a PR in the past to add this check a posteriori, so that I can edit and merge? – Erotica

Yes after creating the pull request, you could check or uncheck the checkbox. Just tested it. – Inconsolable

@Erotica you github link wont work (404). Guess its private? – Inconsolable

It's just a dummy URL just to give future readers an idea of what the URL should look like – Erotica