aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml2
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 16f82a19ee..afed5c4f07 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -451,6 +451,8 @@ pkg:nix:deploy:channel:
- pkg:nix:deploy
script:
- echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
+ # Remove all pr branches because they could be missing when we run git fetch --unshallow
+ - git branch --list 'pr-*' | xargs -r git branch -d
- git fetch --unshallow
- git branch -v
- git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_SHA}":"refs/heads/${CI_COMMIT_REF_NAME}"