diff options
| author | Enrico Tassi | 2019-03-13 11:35:02 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-13 11:35:02 +0100 |
| commit | 63362b21a4fbb5e921ffca723d4eba923fb4e62d (patch) | |
| tree | 54e020974148c135024a51a1726cb1c1c282707d | |
| parent | 915192abdf1bdb3129fd28f05cee6340d5a8c464 (diff) | |
| parent | 288a9d42df805064adfb26daa488fb55d034707a (diff) | |
Merge PR #9739: [dune] [configure] Fix `gramlib` path for hardcoded includes.
Reviewed-by: gares
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index ef38651a4d..8b6fccb5e3 100644 --- a/configure.ml +++ b/configure.ml @@ -1101,7 +1101,7 @@ let write_configml f = pr_b "native_compiler" !prefs.nativecompiler; let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; - "engine"; "pretyping"; "interp"; "gramlib/.pack"; "parsing"; "proofs"; + "engine"; "pretyping"; "interp"; "gramlib"; "gramlib/.pack"; "parsing"; "proofs"; "tactics"; "toplevel"; "printing"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" |