HTML documentation

[Neil Jerram]

I think there was a recent email about adding the current GRM (in
HTML) to the web pages, where Marius mentioned some problems with
texi2html.  (I seem to have lost that email here, so not 100% sure.)

I got problems with texi2html too, and just tried makeinfo --html
--number-sections instead.  makeinfo seems much happier than
texi2html, so perhaps we should switch to that.  Does anyone have a
view on the relative merits of the output produced by texi2html and
'makeinfo --html --number-sections'?  (I think I now prefer makeinfo.)

        Neil