Backport PR coq#19805: Use the release Dune profile when running `con…

…figure` during opam package installation
ppedrot · Jan 20, 2025 · b83bd97 · b83bd97
2 parents 6faa66a + f17318e
commit b83bd97
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 1 deletion.
diff --git a/configure b/configure
@@ -11,4 +11,11 @@ then
     exit 1
 fi
 
-dune exec --root . -- $configure "$@"
+if [ "x$1" = 'x-release' ]; then
+  shift 1
+  dune_release='--profile=release'
+else
+  dune_release=''
+fi
+
+dune exec $dune_release --root . -- $configure "$@"
diff --git a/coq.opam b/coq.opam
@@ -20,6 +20,7 @@ dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
+    "-release" # -release must be the first command line argument
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"

diff --git a/coq.opam.template b/coq.opam.template
@@ -1,6 +1,7 @@
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
+    "-release" # -release must be the first command line argument
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"

diff --git a/rocq-runtime.opam b/rocq-runtime.opam
@@ -39,6 +39,7 @@ dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
+    "-release" # -release must be the first command line argument
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"

diff --git a/rocq-runtime.opam.template b/rocq-runtime.opam.template
@@ -1,6 +1,7 @@
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
+    "-release" # -release must be the first command line argument
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"