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 /dev/ci | |
| parent | 13a5d507049e03497ba17434c5f4089beb3312d6 (diff) | |
| parent | a154a824f96a010acc00bedede888dc894ace2e7 (diff) | |
Merge PR #10047: [opam] [dune] Fix opam build by correctly setting prefix.
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions