[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