aboutsummaryrefslogtreecommitdiff
path: root/topbin
diff options
context:
space:
mode:
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 e35a3de54b..3b861afe78 100644
--- a/topbin/dune
+++ b/topbin/dune
@@ -28,6 +28,11 @@
(libraries coq.toplevel)
(link_flags -linkall))
+(install
+ (section bin)
+ (package coq)
+ (files (coqc_bin.bc as coqc.byte)))
+
; Workers
(executables
(names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin)