Re: [patch][gdb,etc] Add configure option to disable building internal documentation.

[Joel Brobecker <brobecker@adacore.com>]

> Anyhow, consider the viewpoint of a new end-user who has just installed 
> a binary package.  For them, it's unlikely that the GDB documentation is 
> in /usr/local/info; it's probably going to be in /opt/$gdb-package/doc 
> or someplace.  If that was set up with "make install-pdf", there will be 
> four or five manuals in there -- three of which are irrelevant to their 
> needs, and which they don't want.

I agree that such an option would be very useful. I would even consider
changing the default to not installing these docs unless an option is
specified, since I think that most people who do gdb installs only
care about building/installing/using. Even as a GDB developer who
uses this documentation from time to time, I actually never look at
the installed documentation, because I never do "make install"! Most
of the time, I just go on the GDB webpage and browse the documentation
from there.

Anyway, I like the new option. Having the default one way or the other
doesn't matter much to me, so don't let this prevent this idea from
being implemented. We can always change the default later if we want to. 
That's the easy part.

-- 
Joel