Skip to content

Commit

Permalink
Use the release profile for configure in opam
Browse files Browse the repository at this point in the history
The build instructions in the opam files correctly use `-p` for the
builds themselves, but the configure script uses the default profile.
The configure script now recognises -release in its first argument as
meaning that `--profile=release` should be added to the `dune exec`
invocation, and the opam files are updated to include this flag.

(cherry picked from commit 732e987)
  • Loading branch information
dra27 authored and ppedrot committed Jan 20, 2025
1 parent 6faa66a commit f17318e
Show file tree
Hide file tree
Showing 5 changed files with 12 additions and 1 deletion.
9 changes: 8 additions & 1 deletion configure
Original file line number Diff line number Diff line change
Expand Up @@ -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 "$@"
1 change: 1 addition & 0 deletions coq.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions coq.opam.template
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
1 change: 1 addition & 0 deletions rocq-runtime.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions rocq-runtime.opam.template
Original file line number Diff line number Diff line change
@@ -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"
Expand Down

0 comments on commit f17318e

Please sign in to comment.