From 6ecf9b9814222e112a6b81a090aaf710556d7079 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 6 Dec 2024 13:51:40 +0100
Subject: [PATCH] ci-stdlib don't use --release

In particular this makes it respect the user's `display` setting
---
 dev/ci/ci-stdlib.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/ci/ci-stdlib.sh b/dev/ci/ci-stdlib.sh
index 884322952937..a0d1b65d1899 100644
--- a/dev/ci/ci-stdlib.sh
+++ b/dev/ci/ci-stdlib.sh
@@ -8,6 +8,6 @@ ci_dir="$(dirname "$0")"
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "stdlib"
-  dune build -p coq-stdlib @install
+  dune build --root . --only-packages=coq-stdlib @install
   dune install --root . coq-stdlib --prefix="$CI_INSTALL_DIR"
 )