diff options
| author | Gaëtan Gilbert | 2018-11-07 14:47:07 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-07 14:47:07 +0100 |
| commit | 8f09c0667d2566534ab9da77651686904b23aac5 (patch) | |
| tree | 37552eab9571e9c984dd6bd21b2f0b02d1404f62 | |
| parent | 14c55444b3bd574f77b4443916c55f8f102414b6 (diff) | |
| parent | bf513f66ebf4e33a6c923bff0d0c7828dda58acf (diff) | |
Merge PR #8927: Optimise git cloning
| -rw-r--r-- | .gitlab-ci.yml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f5e0fb420a..d866882dbd 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -15,6 +15,7 @@ variables: OPAM_SWITCH: "base" # Used to select special compiler switches such as flambda, 32bits, etc... OPAM_VARIANT: "" + GIT_DEPTH: "1" docker-boot: stage: docker |