gcc-wwwdocs branch master updated. dc50865bf99c3a2abf007bb15c011bdecc583413

[rearnsha@gcc.gnu.org]

This is an automated email from the git hooks/post-receive script. It was
generated because a ref change was pushed to the repository containing
the project "gcc-wwwdocs".

The branch, master has been updated
       via  dc50865bf99c3a2abf007bb15c011bdecc583413 (commit)
      from  b1bd21c81af3bc3098fca4293af164a6c6a4544a (commit)

Those revisions listed above that are new to this repository have
not appeared on any other notification email; so we list those
revisions in full, below.

- Log -----------------------------------------------------------------
commit dc50865bf99c3a2abf007bb15c011bdecc583413
Author: Richard Earnshaw <rearnsha@arm.com>
Date:   Fri Jan 24 15:22:16 2020 +0000

    gitwrite: Move warning about not pushing to other users' spaces
    
    Move the warning about not pushing to other users' spaces to the
    introductory material for personal and vendor branches and adapt to
    cover vendor spaces as well.  Minor tweaks to the original text.

diff --git a/htdocs/gitwrite.html b/htdocs/gitwrite.html
index b5d7ff3..97d6087 100644
--- a/htdocs/gitwrite.html
+++ b/htdocs/gitwrite.html
@@ -378,7 +378,7 @@ The GCC git repository is used by many people and the branch and tag
 namespace would become very polluted if all branches lived at the
 top-level naming space.  To help minimise the amount of data that
 needs to be fetched the git repository on gcc.gnu.org supports
-having personal and vendor branches that developers use to
+having personal and vendor spaces that developers use to
 share their work.  These are not pulled by default, but simple
 configuration steps can give access to them.
 
@@ -391,7 +391,14 @@ configuration steps can give access to them.
     in <code>refs/vendors/<i>vendor-name</i>/tags</code>.</li>
 </ul>
 
-Scripts exist in the contrib directory to help manage these spaces.
+<p><em>Personal and vendor spaces are controlled by the individual
+user or vendor.  Do not push changes to somebody else's space without
+their express permission.</em>  Rather than pushing to somebody
+else's branch, consider pushing to your own personal branch and having
+collaborators pull from there.
+</p>
+
+<p>Scripts exist in the contrib directory to help manage these spaces.</p>
 
 <h3>contrib/gcc-git-customization.sh</h3>
 
@@ -436,12 +443,6 @@ you intend.  The script <code>contrib/git-add-user-branch.sh</code>
 can be used to create a new personal branch which can be pushed and
 pulled from the <i>users/me</i> remote.</p>
 
-<p><em>Personal spaces are controlled by the individual user.  Do not push
-changes to somebody else's space without their express permission.</em>
-(Rather than pushing to somebody else's personal branch, consider pushing
-to your own personal branch and having collaborators pull from there.)
-</p>
-
 <p>The script also defines a few useful aliases that can be used with the
 repository:</p>
 

-----------------------------------------------------------------------

Summary of changes:
 htdocs/gitwrite.html | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)


hooks/post-receive
-- 
gcc-wwwdocs