PATCH: Remove gxxint.texi

[Gerald Pfeifer]

On Tue, 1 May 2001, Joseph S. Myers wrote:
> Here is the corresponding patch to update_web_docs (which also fixes a
> bug: texi2html shouldn't be run on .texi files that aren't present)
> and to onlinedocs/index.html.  OK to commit?

Certainly, certainly.

  2001-04-30  Joseph S. Myers  <jsm28@cam.ac.uk>

	* update_web_docs: Don't generate HTML from gxxint.texi.  Don't
	run texi2html on manuals that aren't present.

(Please also update the version of the script on gcc.gnu.org itself.)

Thanks!

Gerald
-- 
Gerald "Jerry" pfeifer@dbai.tuwien.ac.at http://www.dbai.tuwien.ac.at/~pfeifer/