Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output

2015-03-31 Thread Assaf Gordon
Hello, On Mar 31, 2015, at 11:51, Ludovic Courtès wrote: <...> > , 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://ww

Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output

2015-03-31 Thread Pádraig Brady
On 31/03/15 16:51, Ludovic Courtès wrote: > Reviving this old thread... > http://lists.gnu.org/archive/html/bug-gnulib/2014-12/msg00157.html > > l...@gnu.org (Ludovic Courtès) skribis: > >> The patch below intends to make on-line manuals prettier by default, and >> to make it easier to change the

Re: [PATCH] gendocs.sh: default to a common CSS style sheet for HTML output

2015-03-31 Thread Ludovic Courtès
Reviving this old thread... http://lists.gnu.org/archive/html/bug-gnulib/2014-12/msg00157.html l...@gnu.org (Ludovic Courtès) skribis: > The patch below intends to make on-line manuals prettier by default, and > to make it easier to change their style in the future. > > It assumes that