[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.

0 files changed, 0 insertions, 0 deletions