From 2c0127ff6d528a5c90d7cb553ac0fc3c3ec7ad99 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Sat, 18 Nov 2023 11:41:44 +0100
Subject: [PATCH] CI: delete .git of downloaded projects to reduce artifact
 size

fiat-crypto artifacts seem to hover around 500MB (zipped) which seems
to be the limit. This should reduce that by over 100MB.

(Notably I see pack-dd3467f8c46a76be48de952ac01a5396f376deb6.pack with
compressed size 150MB in the artifacts of https://gitlab.inria.fr/coq/coq/-/jobs/3599481)
---
 dev/ci/ci-common.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 21e5ed058953..00031dd6b638 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -93,8 +93,9 @@ set -x
 # in [$CI_BUILD_DIR/project] if the folder does not exist already;
 # if it does, it will do nothing except print a warning (this can be
 # useful when building locally).
-# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty
+# Note: when there is an overlay, $WITH_SUBMODULES is set to 1 or $CI is unset or empty
 # (local build), it uses git clone to perform the download.
+# If $CI is nonempty it then removes the .git (to reduce artifact size)
 git_download()
 {
   local project=$1
@@ -135,6 +136,9 @@ git_download()
     if [ "$WITH_SUBMODULES" = 1 ]; then
         git submodule update --init --recursive
     fi
+    if [ "$CI" ]; then
+        rm -rf .git
+    fi
     popd
   else # When possible, we download tarballs to reduce bandwidth and latency
     local archiveurl_var="${project}_CI_ARCHIVEURL"