diff --git a/Makefile b/Makefile index 39951f046496d79fdd4333ad42ed245bb9599f80..efe203b784e7ea0d83af951dad81a29212d2018f 100644 --- a/Makefile +++ b/Makefile @@ -33,13 +33,16 @@ $(error \ "You should run ./configure first (or autoconf if there is no configure)") endif +DUNE_BUILD_OPTS?= + RELEASE?=no ifeq ($(RELEASE),yes) -DUNE_BUILD_OPTS=--release -else -DUNE_BUILD_OPTS= +DUNE_BUILD_OPTS+=--release endif +DUNE_DISPLAY?=progress # Dune default, see '--display' dune option +DUNE_BUILD_OPTS+=--display $(DUNE_DISPLAY) + ################### # Frama-C Version # ###################