diff options
| author | Emilio Jesus Gallego Arias | 2019-03-11 19:12:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-11 19:12:13 +0100 |
| commit | 288a9d42df805064adfb26daa488fb55d034707a (patch) | |
| tree | b0b08e39d71d270eb336e1df17239b33a5d1b42e /configure.ml | |
| parent | 74534f84a782f5de740c52cb97b3ca3a02eb6aa2 (diff) | |
[dune] [configure] Fix `gramlib` path for hardcoded includes.
The regular make build uses a non-standard header path for their files
[as a way to workaround the ugliness of the non-hygienic build]
This breaks in Dune as it uses the regular object file pack, so
`coq_makefile` won't find it. We cherry pick a change from #8729 which
fixes the updated version of bug #9735 , even tho `coq_makefile`
should stop relying on hardcoded paths and use findlib instead.
Closes #9735
Diffstat (limited to 'configure.ml')
| -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") "" |