aboutsummaryrefslogtreecommitdiff
path: root/topbin
diff options
context:
space:
mode:
authorThéo Zimmermann2019-03-01 14:30:30 +0100
committerThéo Zimmermann2019-03-01 14:30:30 +0100
commitf37c4445228f5aba5137f397755ebc8cb8c0c482 (patch)
tree20e381f514081c98ac9fe31736036918046c1c3a /topbin
parented5685a2afaa9c429d1f16950317363d9b0bc1a8 (diff)
parentbf385a1134a0b0d4aba971c7b734487937e26b2c (diff)
Merge PR #9006: [dune] Add quickide target for building of IDE.
Reviewed-by: Zimmi48 Reviewed-by: gares
Diffstat (limited to 'topbin')
-rw-r--r--topbin/dune5
1 files changed, 5 insertions, 0 deletions
diff --git a/topbin/dune b/topbin/dune
index f42e4d6fc2..e35a3de54b 100644
--- a/topbin/dune
+++ b/topbin/dune
@@ -36,3 +36,8 @@
(modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin)
(libraries coq.toplevel)
(link_flags -linkall))
+
+; Workers installed targets
+(alias
+ (name topworkers)
+ (deps %{bin:coqqueryworker.opt} %{bin:coqtacticworker.opt} %{bin:coqproofworker.opt}))