From ab9391377bc5279139f4513cbd4224010f98e358 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 17 Dec 2024 13:33:43 +0100
Subject: [PATCH] CI: disable bin_annot (for smaller artifacts)

---
 .gitlab-ci.yml           | 3 +++
 dev/ci/dune-workspace.ci | 3 +++
 2 files changed, 6 insertions(+)
 create mode 100644 dev/ci/dune-workspace.ci

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 98b793e98ab0..a3f7cb125d2d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -83,6 +83,8 @@ before_script:
       - config/dune.c_flags
     expire_in: 1 week
   script:
+    - cp dev/ci/dune-workspace.ci dune-workspace
+
     - PKGS=coq-core,rocq-core,coqide-server
     - if [ "$COQIDE" != "no" ]; then PKGS=${PKGS},coqide; fi
     - dev/ci/gitlab-section.sh start coq.clean coq.clean
@@ -109,6 +111,7 @@ before_script:
   interruptible: true
   extends: .auto-use-tags
   script:
+    - cp dev/ci/dune-workspace.ci dune-workspace
     - make $DUNE_TARGET
     - tar cfj _build.tar.bz2 _build
   variables:
diff --git a/dev/ci/dune-workspace.ci b/dev/ci/dune-workspace.ci
new file mode 100644
index 000000000000..54eb759e9db5
--- /dev/null
+++ b/dev/ci/dune-workspace.ci
@@ -0,0 +1,3 @@
+(lang dune 3.8)
+(context default)
+(env (_ (bin_annot false)))