aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-14 15:48:08 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-17 11:50:41 +0200
commit41489a97014ab60b3dcc0f32dfdd10aacc6bcb98 (patch)
tree652b04fc8b53d2f590151ec53f4b686f56fc694e /tools/coq_makefile.ml
parent99e84da08f7a38ac70d90d21d644b4a9a4a80c91 (diff)
[API] Remove `open API` in ml files in favor of `-open API` flag.
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 43f7670a6..c3aedf538 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -197,7 +197,7 @@ let generate_conf_coq_config oc args bypass_API =
section oc "Coq configuration.";
let src_dirs = if bypass_API
then Coq_config.all_src_dirs
- else Coq_config.api_dirs @ Coq_config.plugins_dirs in
+ else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in
Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args));
;;