@@ -424,25 +424,17 @@ some aliases that might be useful when developing GCC. The script will
settings configured by the script will still be useful.</li>
</ul>
-<p>If you have multiple clones of the gcc repository you can fetch
+<p>If you have personal branches pushed to the gcc repository you can fetch
updates from your personal space by running
- <code>git fetch me</code>
-(or whatever personal prefix you've chosen). You can also push an
-already existing branch using <code>git push me me/branch</code>.
-Beware that if you have more than one personal branch set up locally,
-simply typing <code>git push me</code> will potentially push all such
-personal branches. Use --dry-run to check that what will be pushed is
-what you intend.</p>
-
-<p>To create a new personal branch, the following sequence of steps can be
-used:</p>
-<blockquote><pre>
- git push me <start-ref>:refs/users/<userid>/heads/<topic>
- git fetch me
- git checkout -b me/<topic> remotes/me/<topic>
-</pre></blockquote>
-<p>If you've used a different personal prefix to 'me' then use that
- in the sequence described above.</p>
+<code>git fetch users/me</code> (or whatever personal prefix you've
+chosen). You can also push an already existing branch using <code>git
+push users/me me/branch</code>. Beware that if you have more than one
+personal branch set up locally, simply typing <code>git push
+users/me</code> will potentially push all personal branches based on
+that remote. Use --dry-run to check that what will be pushed is what
+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>The script also defines a few useful aliases that can be used with the
repository:</p>
@@ -523,6 +515,28 @@ This will create the branch both locally and on the server, but will not
check the branch out locally. You can do that afterwards with
<code>git checkout</code> or <code>git worktree</code>.
+<h3>contrib/git-add-user-branch.sh</h3>
+
+<p>before this script can be used, your personal space access should be
+ set up by running <code>contrib/gcc-git-cusomization.sh</code>.</p>
+
+<p>The script takes two arguments, the name of the new branch to create
+ and a <i>ref</i> to create it from. The personal prefix for the new
+ branch is optional and will be automatically added if omitted. For example,
+ if your personal prefix is the default (me), then running:</p>
+
+<blockquote><pre>
+ contrib/git-add-user-branch.sh topic master
+</pre></blockquote>
+
+<p>will set up a branch called <code>topic</code> on the server and a
+ local branch called <code>me/topic</code> that tracks it. The banch
+ can then be pushed using:</p>
+
+<blockquote><pre>
+ git push users/me me/topic
+</pre></blockquote>
+
<hr />
<h2 id="account">Tips&Tricks around your account</h2>