aboutsummaryrefslogtreecommitdiff
path: root/topbin
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-15 15:07:10 +0100
committerEmilio Jesus Gallego Arias2019-03-01 12:44:00 +0100
commitbf385a1134a0b0d4aba971c7b734487937e26b2c (patch)
tree20e381f514081c98ac9fe31736036918046c1c3a /topbin
parented5685a2afaa9c429d1f16950317363d9b0bc1a8 (diff)
[dune] Add quickide target for building of IDE.
Note that `states` doesn't work reliably yet, but that is a separate problem that will be fixed in Dune 1.6. [Or we could also fix it improving the rules in envars.ml]
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}))