diff options
| author | Théo Zimmermann | 2019-05-02 13:20:07 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-02 13:20:07 +0200 |
| commit | 10c3e2ed8c63cbfbd2256fa0c357aa4ccb0ddada (patch) | |
| tree | 53bf317c70dd96b324a35f7c458e919b3660b140 | |
| parent | 13a5d507049e03497ba17434c5f4089beb3312d6 (diff) | |
| parent | a154a824f96a010acc00bedede888dc894ace2e7 (diff) | |
Merge PR #10047: [opam] [dune] Fix opam build by correctly setting prefix.
Reviewed-by: Zimmi48
| -rw-r--r-- | coq.opam | 5 |
1 files changed, 1 insertions, 4 deletions
@@ -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 ] |
