diff options
| author | Emilio Jesus Gallego Arias | 2019-05-02 09:43:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-02 09:43:19 +0200 |
| commit | a154a824f96a010acc00bedede888dc894ace2e7 (patch) | |
| tree | 8d4111d125f546054c3901a0f61bff1c8457caaa /dev/ci | |
| parent | 213b5419136e4639f345e171c086b154c14aa62c (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.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions