texi2html version

[Joseph S. Myers]

At present, gccadmin has its own copy of texi2html (version 1.56k), while
/usr/local/bin/texi2html is version 1.57.

* Is there any particular reason for gccadmin to use its own copy?

* Since the GCC manual uses various more recent texinfo features (@option,
etc.), more recent texi2html versions seem to produce better results on it
than the one currently used for onlinedocs.  Unless there's a particular
reason for gccadmin to have its own older copy, could
/usr/local/bin/texi2html be updated to a more recent version (e.g. 1.64
from http://www.mathematik.uni-kl.de/~obachman/Texi2html/index.html )
(which I'd then make gccadmin use instead of a local copy)?

-- 
Joseph S. Myers
jsm28@cam.ac.uk