diff options
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 |