CI: disable bin_annot (for smaller artifacts)

SkySkimmer · Dec 18, 2024 · fc9eb92 · fc9eb92
1 parent eafed8f
commit fc9eb92
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git 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=rocq-runtime,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
@@ -0,0 +1,3 @@
+(lang dune 3.8)
+(context default)
+(env (_ (bin_annot false)))