aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-05-02 09:43:19 +0200
committerEmilio Jesus Gallego Arias2019-05-02 09:43:19 +0200
commita154a824f96a010acc00bedede888dc894ace2e7 (patch)
tree8d4111d125f546054c3901a0f61bff1c8457caaa
parent213b5419136e4639f345e171c086b154c14aa62c (diff)
[opam] [dune] Fix opam build by correctly setting prefix.
The OPAM build has been broken it seems since almost the beginning as OPAM doesn't substitute variables in the almost undocumented `build-env` form. Packages built this way worked as Coq used a different method to locate `coqlib`, however the value for `coqlib` was incorrect. We set instead the right prefix using an explicit configure call.
-rw-r--r--coq.opam5
1 files changed, 1 insertions, 4 deletions
diff --git a/coq.opam b/coq.opam
index da3f1b518d..05b20e08b6 100644
--- a/coq.opam
+++ b/coq.opam
@@ -25,11 +25,8 @@ depends: [
"num"
]
-build-env: [
- [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
-]
-
build: [
+ [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
[ "dune" "build" "@vodeps" ]
[ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ]
[ "dune" "build" "-p" name "-j" jobs ]