diff --git a/Makefile b/Makefile index efe203b784e7ea0d83af951dad81a29212d2018f..3888fe55efeb6ee3941cb57c904dbd9bf717d913 100644 --- a/Makefile +++ b/Makefile @@ -40,7 +40,10 @@ ifeq ($(RELEASE),yes) DUNE_BUILD_OPTS+=--release endif -DUNE_DISPLAY?=progress # Dune default, see '--display' dune option +# DUNE_DISPLAY: chose Dune build verbosity (see '--display' dune option) +# Default: progress (same as dune default) +# Recommend for tests: short +DUNE_DISPLAY?=progress DUNE_BUILD_OPTS+=--display $(DUNE_DISPLAY) ###################