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

[Robert Kloefkorn]

Hello Markus,

I think it is a bug fix since make dist was not working without WML, nor 
on packages that were made without documentation.
As Andreas said, it makes no sense to force the user to only build tar 
packages with documentation. For official tar balls the documentation 
really makes sense, for all other not because you just don't need it.
So I think my changes are really useful since everything that worked 
before works still in the same way, and additionally now one can build 
slim, only source files containing, packages for installation on 
parallel machines, where one, like in Karlsruhe, normally cannot do a 
checkout of the code.

Regards

Robert