aboutsummaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-10 11:37:09 +0200
committerEmilio Jesus Gallego Arias2018-09-21 01:01:02 +0200
commit81e4c7152da598c1750e7881b197a6fcf54e818d (patch)
tree04b28f3ccc82a436b6202840477a3f5889f98745 /config
parent8f23d8d339403006d6464510c7d2cd285cf38b0a (diff)
[dune] [configure] Allow to set prefix using environment variable.
This is a hack to enable correct OPAM building, the medium-term plan is to avoid having to set a prefix at configure time but instead using a set of rules to locate the Coq library. We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
Diffstat (limited to 'config')
-rw-r--r--config/dune4
1 files changed, 2 insertions, 2 deletions
diff --git a/config/dune b/config/dune
index 30faf1233e..cf2bc71363 100644
--- a/config/dune
+++ b/config/dune
@@ -9,5 +9,5 @@
(rule
(targets coq_config.ml)
(mode fallback)
- (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run)
- (action (chdir %{project_root} (run %{ocaml} configure.ml -local -warn-error yes -native-compiler yes))))
+ (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -native-compiler no))))