diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-12-22 14:11:55 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-12-27 14:19:59 +0100 |
| commit | b37d3f199e4521e2ae20cc96f0f2b04acc36c7cc (patch) | |
| tree | 5286af838087a280405b1cf1c7a3248612e7c5aa /configure.ml | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
[API] remove large file containing duplicate interfaces
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/configure.ml b/configure.ml index 0698d93e2..a86b78ba5 100644 --- a/configure.ml +++ b/configure.ml @@ -1134,7 +1134,7 @@ let write_configml f = pr_b "bytecode_compiler" !Prefs.bytecodecompiler; pr_b "native_compiler" !Prefs.nativecompiler; - let core_src_dirs = [ "config"; "dev"; "kernel"; "library"; + let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; "tactics"; "toplevel"; "printing"; "intf"; "grammar"; "ide"; "stm"; "vernac" ] in @@ -1143,7 +1143,6 @@ let write_configml f = core_src_dirs in pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs; - pr "\nlet api_dirs = [\"API\"; \"clib\"; \"lib\"]\n"; pr "\nlet plugins_dirs = [\n"; let plugins = Sys.readdir "plugins" in @@ -1155,7 +1154,7 @@ let write_configml f = plugins; pr "]\n"; - pr "\nlet all_src_dirs = core_src_dirs @ api_dirs @ plugins_dirs\n"; + pr "\nlet all_src_dirs = core_src_dirs @ plugins_dirs\n"; close_out o; Unix.chmod f 0o444 |