aboutsummaryrefslogtreecommitdiff
path: root/dev/dune
diff options
context:
space:
mode:
Diffstat (limited to 'dev/dune')
-rw-r--r--dev/dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/dune b/dev/dune
index ffa885a008..11e42f97f3 100644
--- a/dev/dune
+++ b/dev/dune
@@ -12,6 +12,7 @@
(deps dune-dbg.in
../checker/coqchk.bc
../topbin/coqc_bin.bc
+ ../ide/coqide_main.bc
; This is not enough as the call to `ocamlfind` will fail :/
top_printers.cma)
(action (copy dune-dbg.in dune-dbg)))