From d53122496152e17170908db3ef94a117dedc27d1 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
Date: Fri, 20 Dec 2024 18:21:01 +0100
Subject: [PATCH] Gitlab CI: change GIT_CLONE_PATH to avoid that the root
 folder is named 'opam'

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b458a4908..f0187a416 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -6,6 +6,7 @@ image: buildpack-deps:stable-scm
 
 variables:
   OPAMJOBS: "2"
+  GIT_CLONE_PATH: "$CI_BUILDS_DIR/opam-coq-archive"
 
 cache:
   paths: