@@ -412,12 +412,15 @@ 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>
+that remote.</p>
+
+<p>Use <code>--dry-run</code> to check that what will be pushed is what
+you intend.
-<p>The script also defines a few useful aliases that can be used with the
+<p>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.
+The script also defines a few useful aliases that can be used with the
repository:</p>
<ul>