aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--config/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/config/dune b/config/dune
index a30fdce9aa..83d1364b0c 100644
--- a/config/dune
+++ b/config/dune
@@ -22,4 +22,4 @@
; Needed to generate include lists for coq_makefile
plugin_list
(env_var COQ_CONFIGURE_PREFIX))
- (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no -bin-annot))))