On 17/06/18 12:11, Bruce Korb wrote: > Hi Pádraig, > > If "texi2html" is out of date, then how do I get HTML? > I want to keep my online docs up to date. If there's a better > way, I'm for that. I confess I don't closely track stuff so > when better ways come around, I need to find out by bumping > into something. This is such a bump. It would be convenient > if I could just tell the script to "make html" and it figured > out how to do that. :) Also, if it cannot (like I didn't have > texi2html installed), it should *FAIL* rather than silently > creating an empty html file. It took an hour of futzing around > to finally figure out that the execution failure of the non- > existent texi2html was silently ignored. :(
I'm not too familiar with these tools TBH, but makeinfo is used to generate html if --texi2html is not passed to this gendocs.sh script. texi2html docs also point to makeinfo being the focus of development now. I've pushed my patch. cheers, Pádraig
