diff options
| -rw-r--r-- | .gitlab-ci.yml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7c9a5c9a31..e6eba7745a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -367,7 +367,8 @@ pkg:nix:deploy:channel: only: variables: - $CACHIX_DEPLOYMENT_KEY - dependencies: + dependencies: [] + needs: - pkg:nix:deploy script: - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null @@ -414,6 +415,10 @@ doc:refman:deploy: - doc:ml-api:odoc - doc:refman:dune - doc:stdlib:dune + needs: + - doc:ml-api:odoc + - doc:refman:dune + - doc:stdlib:dune script: - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy |