aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-02 13:20:07 +0200
committerThéo Zimmermann2019-05-02 13:20:07 +0200
commit10c3e2ed8c63cbfbd2256fa0c357aa4ccb0ddada (patch)
tree53bf317c70dd96b324a35f7c458e919b3660b140
parent13a5d507049e03497ba17434c5f4089beb3312d6 (diff)
parenta154a824f96a010acc00bedede888dc894ace2e7 (diff)
Merge PR #10047: [opam] [dune] Fix opam build by correctly setting prefix.
Reviewed-by: Zimmi48
-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 ]