From d6c59aafb85cb22672f7d39312dc4c6eaee13ae3 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Jul 2023 09:58:23 +0200
Subject: [PATCH] [opam] fix release option in opam installation
---
opam | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/opam b/opam
index fedc35ddc36..7ea652e166d 100644
--- a/opam
+++ b/opam
@@ -98,7 +98,7 @@ build: [
install: [
[make
- "PREFIX=%{prefix}%" "MANDIR=%{man}%"
+ "RELEASE=yes" "PREFIX=%{prefix}%" "MANDIR=%{man}%"
"DOCDIR=%{doc}%" { with-doc }
"install"
]
--
GitLab