diff --git a/opam/opam b/opam/opam index 9edcc76b64062c0aee195cc44862579a16fd4b38..dc071e629a7392ef2ace3b6c12ed2f7d0a5ebd4a 100644 --- a/opam/opam +++ b/opam/opam @@ -87,7 +87,7 @@ tags: [ ] build: [ - ["dune" "build" "-j%{jobs}%" "--release" "@install"] + ["dune" "build" "-j%{jobs}%" "--release" "--promote-install-files=false" "@install"] [make "-C" "doc" "download"] {with-doc} ]