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(-) 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> -- 2.39.0
