From f6bc4b60e354393099f90dce6bdc0dedd5dbae8e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 27 Sep 2022 11:26:27 +0200
Subject: [PATCH] [opam] do not promote install files
---
opam/opam | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/opam/opam b/opam/opam
index 9edcc76b640..dc071e629a7 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}
]
--
GitLab