aboutsummaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-11 17:45:58 +0200
committerThéo Zimmermann2018-10-11 17:45:58 +0200
commit132343514c811e9791d8b5f31de5be8906fab66c (patch)
treeaf65a587474338e6d6c378517bee8a14096af3e7 /config
parent868d5cd983318bff00292329a3920c3b65eb3ada (diff)
parent9e39d88ffb5829a9e2c82fbf54c0765a819b3e5e (diff)
Merge PR #8566: [dune] [test-suite] Support for running the test suite with Dune.
Diffstat (limited to 'config')
-rw-r--r--config/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/config/dune b/config/dune
index ce87a7816d..cc993b97c9 100644
--- a/config/dune
+++ b/config/dune
@@ -7,7 +7,7 @@
; Dune doesn't use configure's output, but it is still necessary for
; some Coq files to work; will be fixed in the future.
(rule
- (targets coq_config.ml)
+ (targets coq_config.ml Makefile)
(mode fallback)
(deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
(action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))