[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML out
|
From: |
Assaf Gordon |
|
Subject: |
Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output |
|
Date: |
Tue, 31 Mar 2015 13:45:31 -0400 |
Hello,
On Mar 31, 2015, at 11:51, Ludovic Courtès <address@hidden> wrote:
<...>
> <http://gnu.org/s/gnulib/manual.css>, and then to update gendocs.sh to
> refer to that by default.
>
> Objections? Suggestions?
This URL results in two redirections, perhaps it'll better to use the expanded
version?
http://www.gnu.org/software/gnulib/manual.css
(see https://debbugs.gnu.org/cgi/bugreport.cgi?bug=18428#49).
-assaf