diff options
| author | Emilio Jesus Gallego Arias | 2018-11-28 17:12:48 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-08 21:35:07 +0100 |
| commit | e245e31a6fa3df465f99159999aac6ebbc0b48eb (patch) | |
| tree | dbf4b6678c9665ee095e752d1ca9de9e5e0a5ca6 /dev/ci/ci-basic-overlay.sh | |
| parent | fa20a54d9fbe0f3872614a592fcef7ef56b05e49 (diff) | |
[dune] Install coq libraries in `%{lib_root}/coq` instead of `lib`
This is what the native Dune Coq version already does, but it is a
problem for Coq Dune too as noted by @vgbl.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions