Re: gendocs.sh and texi2html

[Karl Berry]

     @c The @documentencoding is needed for makeinfo, but not for texi2html.

It should be harmless (if not desirable) for texi2html.  If not, it's a
bug, I expect Patrice would like to know about it.