makefile: DUNE_command_FLAGS

gares · gares · commit ae19a3470cd0 · 2024-06-27T09:47:45.000+02:00
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-dune = @dune $(1) $(DUNE_FLAGS)
+dune = dune $(1) $(DUNE_$(1)_FLAGS)
 
 all:
 	$(call dune,build)
