Suggestion: Explicitly warn to not use GitHub web UI for patches

[Adrian Schmutzler]

Hi,

I've repeatedly made the observation that people who submit PRs with edits
from GitHub's web interface cannot do history edits there when we request
them.

This leads to a lot of frustration both for the reviewers and the
submitters. Eventually, it's mostly one of the following three undesirable
options:

1. The submitter has to clone the repository anyway (as he would have done
in the first place otherwise), and do the edits locally. This typically
leads to additional problems with force-pushing to the existing PR, and in
most cases simply means duplicate work for the submitter.
2. The reviewer (committer) has to do the edits for the submitter.
3. The submitter closes the PR because he does not want to do the same thing
twice.

I have dealt with any of these options multiple times.
Consequently, I think the overall disadvantages of direct GitHub edits
outweigh the advantage of this option for easy submissions.
It's also really frustrating for myself when I have to decide whether I
should invest precious time in doing a git 101 with somebody or have to
leave him behind otherwise.

Thus, I'd like actively discourage this option in submitting-patches, and
edit the current references to this option there accordingly. This
essentially implies something like "Please, do not use GitHub Web UI for
creating commits because ...". Of course, not everybody will read it, but if
it helps for a few of them, it's already better than now.

Are there any (other) opinions out there?
Do we require a vote for that or is it enough if there are no objections
after a certain waiting time?

Best

Adrian