diff options
| author | Vincent Laporte | 2018-12-10 08:01:50 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-12-10 08:01:50 +0000 |
| commit | cb287591722e4d44671eb8c90138cf063ac5b707 (patch) | |
| tree | 1d9828f37dd51847742db3a3218ca05c8bee97b2 | |
| parent | 9c816837de38b8c0766d49d3923b4338012c4fc1 (diff) | |
| parent | e245e31a6fa3df465f99159999aac6ebbc0b48eb (diff) | |
Merge PR #9106: [dune] Install coq libraries in `%{lib_root}/coq` instead of in `lib
| -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 |