[committed] wwwdocs: gitwrite: Structure a section some more

Message ID 20230119093342.36BEB33E96@hamza.pair.com
State Committed
Headers
Series [committed] wwwdocs: gitwrite: Structure a section some more |

Commit Message

Gerald Pfeifer Jan. 19, 2023, 9:33 a.m. UTC
  On the way properly mark up a command-line option.

Pushed. (The diff locks quite bigger than it actually is.)

Gerald
---
 htdocs/gitwrite.html | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)
  

Patch

diff --git a/htdocs/gitwrite.html b/htdocs/gitwrite.html
index e4dadb27..1ffda77a 100644
--- a/htdocs/gitwrite.html
+++ b/htdocs/gitwrite.html
@@ -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>