1 files changed, 2 insertions, 0 deletions

diff --git a/dune b/dune
index f1f966b7fd..787c3c3674 100644
--- a/dune
+++ b/dune
@@ -42,3 +42,5 @@
  (name runtest)
  (package coqide-server)
  (deps test-suite/summary.log))
+
+; (dirs (:standard _build_ci))