[Dune] --disable-documentation.

[Markus Blatt]

Hi,

On Mon, Jul 30, 2007 at 09:51:34AM +0200, Robert Kloefkorn wrote:
> 
> I wanted to make tar balls for my Summer School next week. I want to use
> 1.0, because it's probably more stable then the trunk. I guess until
> next week the beta6 will not be ready. Therefore I just make the tar
> balls myself. It turned out to not that easy.
> I really don't understand what the policy is. When I checkout the
> release branch, configure it and then apply make dist, what should I
> get? The make dist was only working (on my home computer and my office
> machine) when I provided the --disable-documentation option. Then I
> found that the result is exactly the same as the tar balls on the web
> page. Except dune-common where the html-dist was missing.

I just checked. You were right. Now in all modules the documentation
gets build even with disable-documentation and is included into the
tarball. This procedure breaks if wml is not installed, of course.

So reverting your patch is nonsense. It might not be optimal now but
at least every module behaves the same.

Markus