On 14/01/20 13:39 +0000, Richard Earnshaw wrote:
On 14/01/2020 13:37, Jonathan Wakely wrote:
I really think people should be reviewing what they're about to push
before doing it.
OK for wwwdocs?
I'd recommend
git push origin HEAD:<target-branch>
rather than just 'git push'
Otherwise, OK.
Here's a different proposal, which adds your recommendation (in
addition to the simple 'git push') and also tries to address Richi's
concern by simplifying the instructions for checking what you're about
to push.
commit 067f0438c20e740abe71979ff82d5a5ec5bef484
Author: Jonathan Wakely <jwak...@redhat.com>
Date: Tue Jan 14 14:35:46 2020 +0000
Recommend reviewing local changes before pushing them
diff --git a/htdocs/gitwrite.html b/htdocs/gitwrite.html
index 85a0da2d..3b8b18dd 100644
--- a/htdocs/gitwrite.html
+++ b/htdocs/gitwrite.html
@@ -274,7 +274,14 @@ 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,
+make sure your local branch only contains the changes you expect,
+e.g. by reviewing the <code>git status</code> or <code>git log</code> output.
+Once you're ready to publish the changes, do <code>git push</code>,
+or to be more explicit,
+<code>git push origin HEAD:<i><target branch></i></code>,
+where <code><i><target branch></i></code> is the branch on the remote,
+such as <code>master</code> or <code>releases/gcc-9</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,