aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/dune2
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/dune b/ide/dune
index 037b0fcc9e..70a1709f37 100644
--- a/ide/dune
+++ b/ide/dune
@@ -10,6 +10,8 @@
(executable
(name fake_ide)
+ (public_name fake_ide)
+ (package coqide-server)
(modules fake_ide)
(libraries coqide-server.protocol coqide-server.core))