diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 00:41:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-27 16:53:07 +0200 |
| commit | 615c29be047eafac1ec1a9a853afe5a577873771 (patch) | |
| tree | 00aa103a88de575c181755fc082519e26113ca58 /Makefile.dune | |
| parent | 19f5b6a7d467f75b334e769ebe30cf6459c86855 (diff) | |
[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.
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Makefile.dune b/Makefile.dune index cac1bdd6a1..81afa5bb91 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -7,9 +7,6 @@ # DUNEOPT=--display=short BUILD_CONTEXT=_build/default -COQ_CONFIGURE_PREFIX?=_build/install/default - -export COQ_CONFIGURE_PREFIX help: @echo "Welcome to Coq's Dune-based build system. Targets are:" |