Gitlab CI: change GIT_CLONE_PATH to avoid that the root folder is named 'opam'

MSoegtropIMC · MSoegtropIMC · commit d53122496152 · 2024-12-20T18:31:12.000+01:00
diff --git 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:
