aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-20 19:10:27 +0100
committerEmilio Jesus Gallego Arias2018-11-20 19:10:27 +0100
commitf858025ac2e980b8b00fc8428c8b59ae3d27a1c4 (patch)
treecc0337eeaa211bb774a0d07a20173b2b5a63ffba /dev
parentfc9c25270f22e2e34c45d47f0362d543c1bd2421 (diff)
[dune] Only build printers when the ltac plugin is available.
This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be able to have a clean build of core Coq.
Diffstat (limited to 'dev')
-rw-r--r--dev/dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/dune b/dev/dune
index bfa2d525c9..7dfaa616b6 100644
--- a/dev/dune
+++ b/dev/dune
@@ -4,6 +4,7 @@
(synopsis "Coq's Debug Printers")
(wrapped false)
(modules :standard)
+ (optional)
(libraries coq.toplevel coq.plugins.ltac))
(rule