From 260f76d74528bfcd615438bade2e0b33bf11b26b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 13 Apr 2020 15:17:16 +0200
Subject: dune states target: respect user's global verbosity setting

---
 Makefile.dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.dune b/Makefile.dune
index 9e1747a4c3..b002c7709d 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -59,7 +59,7 @@ voboot:
 	@echo "This target is empty and not needed anymore"
 
 states:
-	dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude
+	dune build $(DUNEOPT) dev/shim/coqtop-prelude
 
 NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install
 
-- 
cgit v1.2.3