From 615c29be047eafac1ec1a9a853afe5a577873771 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Sep 2018 00:41:39 +0200
Subject: [configure] [dune] Don't force the Dune user to set envars.

In order to support sending the OPAM prefix to configure via Dune, we
introduced a `COQ_CONFIGURE_PREFIX` variable.

However, this had the pitfall that now the developer had to set it or
else face a hanging build due to configure expecting user input.

While we wait for a larger cleanup in `-prefix`, we introduce a
`no-ask` option in `./configure` that will avoid this problem. If
`-no-ask` is passed to `configure` no interactive question or display
will be shown to the user.
---
 config/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'config')

diff --git a/config/dune b/config/dune
index cf2bc71363..ce87a7816d 100644
--- a/config/dune
+++ b/config/dune
@@ -10,4 +10,4 @@
  (targets coq_config.ml)
  (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 -native-compiler no))))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
-- 
cgit v1.2.3