diff options
| author | Emilio Jesus Gallego Arias | 2018-11-20 19:10:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-20 19:10:27 +0100 |
| commit | f858025ac2e980b8b00fc8428c8b59ae3d27a1c4 (patch) | |
| tree | cc0337eeaa211bb774a0d07a20173b2b5a63ffba /dev/dune | |
| parent | fc9c25270f22e2e34c45d47f0362d543c1bd2421 (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/dune')
| -rw-r--r-- | dev/dune | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -4,6 +4,7 @@ (synopsis "Coq's Debug Printers") (wrapped false) (modules :standard) + (optional) (libraries coq.toplevel coq.plugins.ltac)) (rule |
