On Sat, 19 Oct 2019, Gerald Pfeifer wrote: > And this makes it a bit nicer (and shorter).
And this makes the anonymous checkout of wwwdocs simple copy&paste. Commmitted. Gerald diff --git a/htdocs/about.html b/htdocs/about.html index 48918c8..a67e358 100644 --- a/htdocs/about.html +++ b/htdocs/about.html @@ -59,8 +59,11 @@ and SSH installed, you can check out the web pages via</p> <p>where <i>username</i> is your user name at gcc.gnu.org.</p> -<p>For anonymous access, use -<code>git://gcc.gnu.org/git/gcc-wwwdocs.git</code> instead.</p> +<p>For anonymous access, use</p> +<blockquote><pre> +<code>git clone git://gcc.gnu.org/git/gcc-wwwdocs.git</code> +</pre></blockquote> +
