From 5b813102d30dc9e4756283967469af94c3705207 Mon Sep 17 00:00:00 2001 From: Kate Date: Wed, 2 Oct 2024 15:25:25 +0100 Subject: [PATCH] debug --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index bc81e833f5b..c95465d4e2c 100644 --- a/Makefile +++ b/Makefile @@ -37,7 +37,7 @@ ALWAYS: @ DUNE_DEP = $(DUNE_EXE) -JBUILDER_ARGS ?= +JBUILDER_ARGS ?= --verbose DUNE_ARGS ?= $(JBUILDER_ARGS) DUNE_PROFILE ?= release