ci-stdlib don't use --release

In particular this makes it respect the user's `display` setting
SkySkimmer · Dec 6, 2024 · 6ecf9b9 · 6ecf9b9
1 parent 476460f
commit 6ecf9b9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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"
 )