diff options
| author | Emilio Jesus Gallego Arias | 2018-11-06 18:52:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-13 12:11:47 +0100 |
| commit | 76048d675212211b623616da7132826d1ee41870 (patch) | |
| tree | 2c288575c13d40cadd30b88e057560c2b2d5ce55 /configure.ml | |
| parent | 0b816e4df10d961cce082894f5e4087dc1c95f01 (diff) | |
[configure] Remove grammar and dev from core_src_dirs.
These directories don't contain Coq sources but internal developer
files. This can create problems, for example, in #8919.
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 39c65683ff..47f7633ae8 100644 --- a/configure.ml +++ b/configure.ml @@ -1211,10 +1211,9 @@ let write_configml f = pr_b "bytecode_compiler" !prefs.bytecodecompiler; pr_b "native_compiler" !prefs.nativecompiler; - let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; + let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; - "tactics"; "toplevel"; "printing"; - "grammar"; "ide"; "stm"; "vernac" ] in + "tactics"; "toplevel"; "printing"; "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 |