On Jun 20, 2001, Guido Draheim <[EMAIL PROTECTED]> wrote:

>> /usr/local/[man|info] for local packages
>> and reserves
>> /opt/[man|info] for "add-on" packages.

> Indeed! so in fact, it should still be $prefix/man etcetera,

Yep

> which leads me to the question where the /doc should go under,

Perhaps instead of --docdir we should have --doc-prefix, that defaults
to --prefix?  Then man, info, html, etc would all be in /usr/local by
default, but this could be easily overridden using --doc-prefix.

Another idea is to have mandir and infodir default to
prefix/{man,info} if --docdir is not specified (in which case it would
default to ${datadir}/doc, and to $doc_prefix/{man,info} otherwise
(not overriding --mandir or --infodir, of course).  Yes, I agree this
is messier to implement and describe, but it seems to make installers'
and distributors' lives simpler.

> Again, the docdir looks like a fairly standard directory,
> so it should be added to the defaultset of configure options.

The problem of adding configure options is that, in a multi-package
build (think of the so-called Cygnus top-level configure), all
configure scripts must accept the same set of options, even if they
ignore some, otherwise you can't use these options for any of the
packages.

-- 
Alexandre Oliva   Enjoy Guarana', see http://www.ic.unicamp.br/~oliva/
Red Hat GCC Developer                  aoliva@{cygnus.com, redhat.com}
CS PhD student at IC-Unicamp        oliva@{lsd.ic.unicamp.br, gnu.org}
Free Software Evangelist    *Please* write to mailing lists, not to me

Reply via email to