From c054dda76825435019ad1b29f7f4292d937d98f9 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Tue, 30 May 2017 10:49:41 +0200 Subject: Add support for "-bypass-API" argument of "coq_makefile" Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac --- configure.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'configure.ml') diff --git a/configure.ml b/configure.ml index a5204d5b5..316cea5c9 100644 --- a/configure.ml +++ b/configure.ml @@ -1088,7 +1088,19 @@ let write_configml f = pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); pr_b "no_native_compiler" (not !Prefs.nativecompiler); + + let core_src_dirs = [ "config"; "dev"; "kernel"; "library"; + "engine"; "pretyping"; "interp"; "parsing"; "proofs"; + "tactics"; "toplevel"; "printing"; "intf"; + "grammar"; "ide"; "stm"; "vernac" ] in + let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") + "" + core_src_dirs in + + pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs; + pr "\nlet api_dirs = [\"API\"; \"lib\"]\n"; pr "\nlet plugins_dirs = [\n"; + let plugins = Sys.readdir "plugins" in Array.sort compare plugins; Array.iter @@ -1097,6 +1109,9 @@ let write_configml f = if Sys.is_directory f' && f.[0] <> '.' then pr " %S;\n" f') plugins; pr "]\n"; + + pr "\nlet all_src_dirs = core_src_dirs @ api_dirs @ plugins_dirs\n"; + close_out o; Unix.chmod f 0o444 -- cgit v1.2.3