From c5213ab2a33087286a7ef224b8d2c73f8d19176d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 14:24:23 +0100
Subject: Fix dune runtest invocation

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

diff --git a/Makefile.dune b/Makefile.dune
index d201d1783a..3d930cf47c 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -53,7 +53,7 @@ quickopt: voboot
 	dune build $(DUNEOPT) $(QUICKOPT_TARGETS)
 
 test-suite: voboot
-	dune $(DUNEOPT) runtest
+	dune runtest $(DUNEOPT)
 
 release: voboot
 	dune build $(DUNEOPT) -p coq
-- 
cgit v1.2.3