[Dune-devel] [Dune-Bugs] [#1211] [PATCH] dunecontrol: allow arguments to the 'make' command

[Christoph Grüninger]

Hi Andreas,
I am glad to hear that your use case works.

> the problem is that this feature is quite underdocumentedand not
 > discoverable at all: [..] would you mind updating the documentation?

It is described in the buildsystem-howto, MAKE_FLAGS is even part of an 
example.
If you have an idea how to improve the documentation, I will apply any 
patches with joy. I want to make the Dune user wiki the place to go for 
documentation, but have not yet found the time to start this project.

Bye
Christoph

-- 
Es ist ja nicht zu leugnen: Hinter dem Schleier der Unwissenheit
lässt sich in etlichen Hinsichten irritationsfreier existieren.
(Hermann Lübbe, dt. Philosoph, *1926)