[Dune] --disable-documentation.
Markus Blatt
Markus.Blatt at ipvs.uni-stuttgart.de
Mon Jul 30 08:47:12 CEST 2007
Hi,
On Sun, Jul 29, 2007 at 04:07:52PM +0200, Robert Kloefkorn wrote:
>
> I suggest to switch the default for building of documentation to
> disabled. When using the tar balls from the web the docu should have
> been build already.
Actually the built documentation is already distributed since one of
the first beta releases. Therefore --enable-documentation had no
effect at all. Unfortunately there is still the bug make clean
removing all documentation. I will fix this this week,
Switching to --disable-documentation would probably prevent the
documentation from being installed. IMHO that is not what a user
wants.
> For people using the trunk we have the docu on the
> web. Therefore, the most common case is not to build the docu. Therefore
> I suggest to switch from --disable-documentation to
> --enable-documentation for people who really want that.
>
I do not care how it is done here. I can live with both.
Markus
More information about the Dune
mailing list