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 | |
| 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.
| -rw-r--r-- | tools/coq_dune.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 41057a79e0..06ad9e4792 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -193,8 +193,8 @@ let pp_dep dir fmt oo = match oo with let out_install fmt dir ff = let itarget = String.concat "/" dir in let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in - let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (bpath [itarget;tg]) in - fprintf fmt "(install@\n @[(section lib)@\n(package coq)@\n(files @[%a@])@])@\n" + let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in + fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" (pp_list pp_ispec sep) ff (* For each directory, we must record two things, the build rules and |