aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorThéo Zimmermann2019-12-06 10:55:51 +0100
committerThéo Zimmermann2019-12-06 10:55:51 +0100
commitf76a6a2444dbc80bfcb46c88449f62d76b6f4984 (patch)
tree953c424a5ad2115a64972e60132a28d1f7a14f40 /ide
parent0e694678eddaede188335df139ce17d649c013e6 (diff)
parent1d454c7721a429490165d1147313c061164b0b66 (diff)
Merge PR #11174: [dune] Update to dune language version 2.0
Reviewed-by: Zimmi48
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 7200915593..a599be9351 100644
--- a/ide/dune
+++ b/ide/dune
@@ -21,6 +21,7 @@
(package coqide-server)
(modules idetop)
(libraries coq.toplevel coqide-server.protocol)
+ (modes native byte)
(link_flags -linkall))
(install
@@ -45,6 +46,7 @@
(name coqide_main)
(public_name coqide)
(package coqide)
+ (optional)
(modules coqide_main)
(libraries coqide_gui))