I really think people should be reviewing what they're about to push
before doing it.
OK for wwwdocs?
commit 2c54cb9e98fe67096b62718d8dbd3b2ca485ff89
Author: Jonathan Wakely <jwak...@redhat.com>
Date: Tue Jan 14 13:34:02 2020 +0000
Recommend reviewing local changes before pushing them
diff --git a/htdocs/gitwrite.html b/htdocs/gitwrite.html
index 85a0da2d..98ac7201 100644
--- a/htdocs/gitwrite.html
+++ b/htdocs/gitwrite.html
@@ -274,7 +274,13 @@ made after you called <code>git add</code> for
them.</strong></li>
<li>After exiting the editor, Git will check in your
changes <strong>locally</strong>. When your prompt returns
the <strong>local</strong> checkin is finished, but you still need to
-push the changes to the shared repository; do <code>git push</code>.
+push the changes to the shared repository. Before pushing it to gcc.gnu.org,
+review your local changes to make sure your local branch only contains
+the changes you expect, e.g. <code>git log @{u}..</code> or
+<code>git diff @{u}</code> (where <code>@{u}</code> refers to the upstream
+branch, most likely something like <code>origin/master</code> or
+<code>origin/releases/gcc-9</code>).
+Once you're ready to publish the changes, do <code>git push</code>.
A message will be sent to the gcc-cvs mailing list indicating that a
change was made. If <code>git push</code> gives an error because
someone else has pushed their own changes to the same branch,
