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 /dev/header.c | |
| 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 'dev/header.c')
0 files changed, 0 insertions, 0 deletions