aboutsummaryrefslogtreecommitdiff
path: root/topbin/dune
diff options
context:
space:
mode:
Diffstat (limited to 'topbin/dune')
-rw-r--r--topbin/dune10
1 files changed, 9 insertions, 1 deletions
diff --git a/topbin/dune b/topbin/dune
index 52f472d149..f42e4d6fc2 100644
--- a/topbin/dune
+++ b/topbin/dune
@@ -20,11 +20,19 @@
(modes byte)
(link_flags -linkall))
+(executable
+ (name coqc_bin)
+ (public_name coqc)
+ (package coq)
+ (modules coqc_bin)
+ (libraries coq.toplevel)
+ (link_flags -linkall))
+
; Workers
(executables
(names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin)
(public_names coqqueryworker.opt coqtacticworker.opt coqproofworker.opt)
(package coq)
- (modules :standard \ coqtop_byte_bin coqtop_bin)
+ (modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin)
(libraries coq.toplevel)
(link_flags -linkall))