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

[Markus Blatt]

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