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

[Mark Kettenis]

> Date: Thu, 08 Nov 2007 00:22:39 +0200
> From: Eli Zaretskii <eliz@gnu.org>
> 
> > Date: Wed, 07 Nov 2007 11:22:12 -0800
> > From: Brooks Moses <brooks@codesourcery.com>
> > CC:  gdb-patches@sourceware.org
> > 
> > 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.  And it's not entirely obvious which 
> > one the user wants to look at first, if they are unfamiliar with GDB and 
> > have a question they want to find an answer to.  That seems confusing to 
> > me, and is clutter in the sense that that's a considerable quantity of 
> > bloat in the package size and its disk-space requirements that is 
> > essentially pointless.
> 
> I really don't feel we are entitled to second-guess the user's needs.
> The manuals that come with GDB are all useful one way or the other;
> it's up to the user to remove those she knows she will never need.
> 
> > Add up the sizes of the pdf, info, and html files, and the space
> > usage is considerable.
> 
> Actually, I doubt it's considerable by modern standards, but even if
> it is, why would someone want to install all 3 formats by default?
> You only need one (any one).

Seconded.  My biggest gripe about Linux these days is the insane
subdivision in subpackages just to save a few megabytes of disk space.