From 288a9d42df805064adfb26daa488fb55d034707a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 11 Mar 2019 19:12:13 +0100
Subject: [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
---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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")
                                     ""
-- 
cgit v1.2.3