From 4d966c4589b199ec81138ca70cff91823d22d064 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 22 Sep 2021 11:25:39 +0200
Subject: [PATCH] [build] Set dune root explicitly / use --release

This should fix #14915 , the problem arises with layouts of the form:

```
foo/dune-project
foo/_opam/bar/dune-project
```

so when inside `foo/_opam/bar`, dune will switch to `foo` as the
project root, for example for `dune build` or `dune exec` , however,
as `_opam` is an ignored dir by default in the `foo` context, the
command will fail.

So indeed, it turns out `--profile release` is not enough, but
`--release` must be used when configured for install.

Thanks a lot to Kate for the help!
---
 Makefile.common            | 2 +-
 configure                  | 2 +-
 tools/configure/cmdArgs.ml | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Makefile.common b/Makefile.common
index ae5148632964..d3dadef1c54a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -116,7 +116,7 @@ DOCGRAM_SOURCE_FILES=$(shell find $(addprefix $(COQ_SRC_DIR)/, doc/tools/docgram
 # Override for developer build [to get warn-as-error for example]
 _DDISPLAY?=quiet
 _DPROFILE?=$(CONFIGURE_DPROFILE)
-_DOPT:=--display $(_DDISPLAY) --profile=$(_DPROFILE)
+_DOPT:=--display=$(_DDISPLAY) $(_DPROFILE)
 _DBUILD:=$(FLOCK) .dune.lock dune build $(_DOPT)
 
 # We rerun dune when any of the source files have changed
diff --git a/configure b/configure
index 53b8dad87355..c0c5dbd6797f 100755
--- a/configure
+++ b/configure
@@ -11,4 +11,4 @@ then
     exit 1
 fi
 
-dune exec -- $configure "$@"
+dune exec --root . -- $configure "$@"
diff --git a/tools/configure/cmdArgs.ml b/tools/configure/cmdArgs.ml
index e0f8989434e8..a8e0746a79b3 100644
--- a/tools/configure/cmdArgs.ml
+++ b/tools/configure/cmdArgs.ml
@@ -71,7 +71,7 @@ let default = {
     if os_type_win32 || os_type_cygwin then NativeNo else NativeOndemand;
   coqwebsite = "http://coq.inria.fr/";
   warn_error = false;
-  dune_profile = "release";
+  dune_profile = "--release";
   install_enabled = true;
 }
 
@@ -79,7 +79,7 @@ let devel state = { state with
   bin_annot = true;
   annot = true;
   warn_error = true;
-  dune_profile = "dev";
+  dune_profile = "--profile=dev";
   interactive = true;
   prefix = Some (Filename.concat (Sys.getcwd ()) "_build_vo/default");
   install_enabled = false;