aboutsummaryrefslogtreecommitdiff
path: root/topbin
diff options
context:
space:
mode:
Diffstat (limited to 'topbin')
-rw-r--r--topbin/dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/topbin/dune b/topbin/dune
index 7b77826216..46052c81e5 100644
--- a/topbin/dune
+++ b/topbin/dune
@@ -26,6 +26,7 @@
(package coq)
(modules coqc_bin)
(libraries coq.toplevel)
+ (modes native byte)
; Adding -ccopt -flto to links options could be interesting, however,
; it doesn't work on Windows
(link_flags -linkall))