diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-05-30 10:49:41 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-12 16:43:32 +0200 |
| commit | c054dda76825435019ad1b29f7f4292d937d98f9 (patch) | |
| tree | d2e921256915fe30c2511f52f8feeb2519e359f1 /configure.ml | |
| parent | a2e1e2fa4f0a005e07972488b6ce6ad59404bd2c (diff) | |
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
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 15 |
1 files changed, 15 insertions, 0 deletions
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 |