* update_web_docs: Use /usr/local/bin/texi2html rather than