Committed. My first git push to the new wwwdocs repository ;-) Thank you, Joseph and everyone else who helped!
Gerald >From 6df815817051ed1defc13eda2cbadc089da6d646 Mon Sep 17 00:00:00 2001 From: Gerald Pfeifer <ger...@pfeifer.com> Date: Thu, 17 Oct 2019 10:19:42 +0200 Subject: [PATCH] Improve markup/nicer formatting for GIT instructions. --- htdocs/about.html | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/htdocs/about.html b/htdocs/about.html index 019b6fbd..a812a7f9 100644 --- a/htdocs/about.html +++ b/htdocs/about.html @@ -53,10 +53,10 @@ a higher chance of being implemented soon. ;-)</p> <p>Assuming you have both git and SSH installed, you can check out the web pages as follows:</p> -<ol> - <li><code>git clone git+ssh://<i>username</i>@gcc.gnu.org/git/gcc-wwwdocs.git</code> - where <i>username</i> is your user name at gcc.gnu.org</li> -</ol> +<blockquote><pre> +<code>git clone git+ssh://<i>username</i>@gcc.gnu.org/git/gcc-wwwdocs.git</code> +where <i>username</i> is your user name at gcc.gnu.org +</pre></blockquote> <p>For anonymous access, use <code>git://gcc.gnu.org/git/gcc-wwwdocs.git</code> instead.</p> -- 2.23.0
