aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-04 16:32:49 +0100
committerEmilio Jesus Gallego Arias2019-03-04 16:32:49 +0100
commit18bdabf7211508e72ece347bbc619f16e79e3678 (patch)
tree4db3ec9d2c87490b237f646f30b73684d0e354c0
parentbe15d32ad16104c81f4fbf42556067848aa0acec (diff)
[dune] [ide] Don't install the internal CoqIDE UI library.
This library is unstable and not meant to be consumed by anyone. We thus make it private.
-rw-r--r--ide/dune5
1 files changed, 2 insertions, 3 deletions
diff --git a/ide/dune b/ide/dune
index 5e3886624c..3618e4f05d 100644
--- a/ide/dune
+++ b/ide/dune
@@ -25,8 +25,7 @@
; IDE Client
(library
- (name gui)
- (public_name coqide.gui)
+ (name coqide_gui)
(wrapped false)
(modules (:standard \ document fake_ide idetop coqide_main))
(optional)
@@ -42,7 +41,7 @@
(public_name coqide)
(package coqide)
(modules coqide_main)
- (libraries coqide.gui))
+ (libraries coqide_gui))
; FIXME: we should install those in share/coqide. We better do this
; once the make-based system has been phased out.