From mboxrd@z Thu Jan 1 00:00:00 1970
Return-Path:
Received: by sourceware.org (Postfix, from userid 2142)
id 53A663858C52; Thu, 19 Jan 2023 09:32:58 +0000 (GMT)
DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 53A663858C52
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sourceware.org;
s=default; t=1674120778;
bh=iwqKSt2yQ+qD1vuYMVj9v9tacDbDsfpTtddFeDcEV70=;
h=To:Subject:Date:From:From;
b=RG+qFrOHhbtmB9BRXsMpaqq+DMpaZkqcPHjXWluC2hKOZqmQayz4vBw/jNxQb3ZlD
SKVMpCKCsHCm5kUecLQVyz7vvCr06LuUQCR3GcZRFvBYsWBFZi8pGd5804/VAeksgF
SFOs6Nvx0hdB9vYJWc0Cu2yQ4pi7C2SpjaiLawhc=
To: gcc-cvs-wwwdocs@gcc.gnu.org
Subject: gcc-wwwdocs branch master updated. 733c9e4ecbcb5c548863fcf88fc1a5b12e68a2d5
X-Git-Refname: refs/heads/master
X-Git-Reftype: branch
X-Git-Oldrev: 66b75e896c9a9daea844281c13aba4ddcd2b82ef
X-Git-Newrev: 733c9e4ecbcb5c548863fcf88fc1a5b12e68a2d5
Message-Id: <20230119093258.53A663858C52@sourceware.org>
Date: Thu, 19 Jan 2023 09:32:58 +0000 (GMT)
From: Gerald Pfeifer
List-Id:
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 733c9e4ecbcb5c548863fcf88fc1a5b12e68a2d5 (commit)
from 66b75e896c9a9daea844281c13aba4ddcd2b82ef (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 733c9e4ecbcb5c548863fcf88fc1a5b12e68a2d5
Author: Gerald Pfeifer
Date: Thu Jan 19 10:32:10 2023 +0100
gitwrite: Structure a section some more
On the way properly mark up a command-line option.
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 git
push users/me me/branch
. Beware that if you have more than one
personal branch set up locally, simply typing git push
users/me
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 contrib/git-add-user-branch.sh
-can be used to create a new personal branch which can be pushed and
-pulled from the users/me remote.
+that remote.
+
+Use --dry-run
to check that what will be pushed is what
+you intend.
-
The script also defines a few useful aliases that can be used with the
+
The script contrib/git-add-user-branch.sh
+can be used to create a new personal branch which can be pushed and
+pulled from the users/me remote.
+The script also defines a few useful aliases that can be used with the
repository:
-----------------------------------------------------------------------
Summary of changes:
htdocs/gitwrite.html | 13 ++++++++-----
1 file changed, 8 insertions(+), 5 deletions(-)
hooks/post-receive
--
gcc-wwwdocs