diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-29 14:08:57 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-29 14:08:57 +0100 |
| commit | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (patch) | |
| tree | cd14828b3c41252961c3bb975e814541ed3c3b78 /configure.ml | |
| parent | 53ade7982bebc8a85133d6b5ba257962e2f3fc15 (diff) | |
| parent | 2be81020d8533b7d275f820fad8f597929aa064e (diff) | |
Merge PR #6493: [API] remove large file containing duplicate interfaces
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 |