From 55e54479837cc70a5c070220a0bf32d0bbf55212 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 7 Dec 2019 18:28:29 +0100
Subject: [configure] [dune] Fix configure under Dune in 32bit builds.

`dev/header.c` is not registered as a dependency, so the configure
step under dune fails in 32bit builds.

Note we don't detect the problem due to dubious code in configure
ignoring stderr messages on process calls.
---
 config/dune | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/config/dune b/config/dune
index a303774e17..5f2f7b1222 100644
--- a/config/dune
+++ b/config/dune
@@ -9,5 +9,9 @@
 (rule
  (targets coq_config.ml coq_config.py Makefile dune.c_flags)
  (mode fallback)
- (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
+ (deps
+   %{project_root}/configure.ml
+   %{project_root}/dev/ocamldebug-coq.run
+   %{project_root}/dev/header.c
+  (env_var COQ_CONFIGURE_PREFIX))
  (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
-- 
cgit v1.2.3