aboutsummaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-26 22:49:20 +0200
committerEmilio Jesus Gallego Arias2018-10-11 14:32:33 +0200
commit9e39d88ffb5829a9e2c82fbf54c0765a819b3e5e (patch)
tree09f31d1d171db723e39d73e7171ff996963a2cc3 /config
parentdc5dbc992727fb807fa56763f8f71d79f598fd6a (diff)
[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))))