[Dune] [Dune-Commit] dune-common r5021 - in trunk/doc: . devel doxygen

Andreas Dedner dedner at mathematik.uni-freiburg.de
Wed Dec 5 18:47:26 CET 2007


Why does the distribution have to include the documentation?
The problem occurs in the following real world application:
compile dune on a parallel machine like in Karlsruhe.
The easiest way is to run a make dist in your local dune-???
on your local computer, transfer the tar balls to the parallel
machine, and run dune-control.
In this case one does not need or want to have any documentation
included!
The fewer dependencies on not really essential packages
there are the better IMHO.
Andreas



Markus Blatt wrote:
> On Wed, Dec 05, 2007 at 03:57:22PM +0100, robertk at dune-project.org wrote:
>> Log:
>> bug fix, make dist did not work without wml installed.
>>
>>
> 
> Why is this supposed to be a bug?????
> 
> If you don't have wml you shouldn't do a make dist as the distribution
> will not be complete (and make install will not work!). It absolutely
> makes sense for make dist to fail if wml is not installed.
> 
> IMHO there was no bug, but there is now.
> Please revert this patch.
> 
> Markus
> 
> _______________________________________________
> Dune mailing list
> Dune at dune-project.org
> http://lists.dune-project.org/mailman/listinfo/dune




More information about the Dune mailing list