diff options
| author | Emilio Jesus Gallego Arias | 2019-12-07 18:28:29 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-07 18:33:43 +0100 |
| commit | 55e54479837cc70a5c070220a0bf32d0bbf55212 (patch) | |
| tree | bf3980d0ae636b9a3500146c2e5e3032c32cf0fc /config | |
| parent | 756d2f4db5eae51c8c01a40550b8c4553bd30f53 (diff) | |
[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.
Diffstat (limited to 'config')
| -rw-r--r-- | config/dune | 6 |
1 files changed, 5 insertions, 1 deletions
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)))) |