Re: Making texi2html optional?

[John Mandereau]

On 2008/08/29 10:49 -0300, Han-Wen Nienhuys wrote:
> 500k ???

It's worse than 500k, and maybe other files are necessary:
189K texi2html.init
493K texi2html.pl
 88K translations.pl

Patrice Dumas develops texi2html a lot these days in order to make it
replace makeinfo, so I definitely agree that adding it in our tree is
not an option: the initial commit and subsequent updates would bloat up
Git history and the sources tarball.


> That's too much.  I can put texi2html in GUB (GUB easily builds from
> CVS and Git repos), to make the default docs use the latest and
> greatest.

Very cool!  I'm going to do required changes in makefiles in
dev/texi2html; as soon as I've checked that "make web" works well with
either "makeinfo --html" or texi2html, I'll merge dev/texi2html into
master.  Reinhold, are you OK with this?

Cheers,
John