Bob Friesenhahn wrote: > I am against having separate install targets because GNU makefiles > normally install everything by default and that is what users should > expect. Installing everything is not a problem for distribution > maintainers since they decide which files to package using their > distribution tools.
When you have a tool that produces so many doc formats, I think you want to be able to let the user select what is wanted. If "make install" implies installing html, then it implies building it, too. That means "make" needs to imply making the html. Probably the friendliest thing is to let the user select at, say, configure time which form(s) of documentation they want built and installed. --enable-html, --disable-info, --enable-ps, etc. with certain defaults for certain output types. Then, the debate degenerates into whether html should default to enabled or disabled. I'd lean toward disabled, but I don't care much either way....
