wwwdocs/htdocs/install -> texinfo

[Joseph S. Myers]

On Sat, 12 May 2001, Gerald Pfeifer wrote:

> Thanks a lot! I just committed this as gcc/doc/install.texi with the

This means the old install manual should be renamed to install-old.texi,
until its contents can be merged into the new manual.  (update_web_docs
expects .texi file names to be unique throughout the source tree.)  
Better, of course, if it moves direct to doc/install-old.texi, along with
the rest of the .texi manuals from the gcc directory.  (I'd rather someone
else deals with doing this move and having the working makefile
infrastructure - then I'll start on moving stuff out of gcc.texi, etc..)

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