aboutsummaryrefslogtreecommitdiff
path: root/dev/dune
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-09 19:27:37 +0100
committerGaëtan Gilbert2018-11-20 13:02:04 +0100
commitd7172fbf2d7ae98ea0471a58c21f93671280d50e (patch)
tree0da78b3ce4563460b245eb641acb3d911fd85390 /dev/dune
parent4d26550af26c1dab464253cc470e8a876fee0025 (diff)
Fix dune-dbg using checker/main -> checker/coqchk
Diffstat (limited to 'dev/dune')
-rw-r--r--dev/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/dune b/dev/dune
index bfa2d525c9..29a20ac17f 100644
--- a/dev/dune
+++ b/dev/dune
@@ -9,7 +9,7 @@
(rule
(targets dune-dbg)
(deps dune-dbg.in
- ../checker/main.bc
+ ../checker/coqchk.bc
../topbin/coqtop_byte_bin.bc
; This is not enough as the call to `ocamlfind` will fail :/
top_printers.cma)