From: Gavin Sinclair <gsinclair@...>
Date: 2004-01-06T14:32:28+09:00
Subject: Re: Best way to install ri documentation -- please check this


>> Or, as I'm sensing some resistance here, should we simply change it so
>>  that end-users need to do an explicit
>>
>>     make doc
>
> I prefer this.  Folks?

Philosophically, developers (the minority) should sacrifice some
convenience so that users (the majority) can have more convenience.  Also,
I believe the documentation should be considered (almost) as important as
the software.  It's an investment in the language.

A configure-time option, either to enable or disable documentation, is the
most appropriate solution; it only needs to be set once.  Given the
philosophical statement above, the *default* should be to *install*
documentation.

Conclusion: I prefer a configure-time option to *disable* documentation.

> Regards,
> // NaHi

Gavin