diff options
| author | Théo Zimmermann | 2019-08-22 18:42:01 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-22 18:42:01 +0200 |
| commit | c2b9df20204a60bc23535648ff772c4faab45851 (patch) | |
| tree | 89c048715dcfe086162f05153ca44a260ea228ce | |
| parent | edd7519b6e1af6d62194f9f3dcc938534b86d036 (diff) | |
[gitlab/ci] Deploy sooner thanks to new needs keyword.
| -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 |