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

[Karl Berry]

I don't agree with changing the default css in gendocs.sh.  (And I also
don't want to debate it, sorry.) If you want to do that for your
manuals, you can use --html or override MAKEINFO or probably other
things.

k