aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-20 01:38:53 +0100
committerEmilio Jesus Gallego Arias2019-03-20 01:38:53 +0100
commit19bb153e049dcd7bd3ce4780e9fe18ec1d3a1169 (patch)
tree1c484a78dfcd04e95c5918583996eb454f02190f
parent0a2773c90b69e301ec1d7203e8188694244b0167 (diff)
parent98a779d411b3299d3990dd4932ff52e053789706 (diff)
Merge PR #9805: [CI] Push the right commit to cachix
-rw-r--r--.gitlab-ci.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 828380894e..e688fbd463 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -359,7 +359,7 @@ pkg:nix:deploy:channel:
- echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
- git fetch --unshallow
- git branch -v
- - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_REF_NAME}"
+ - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_SHA}":"${CI_COMMIT_REF_NAME}"
pkg:nix:
extends: .nix-template