aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-09-24 14:53:04 +0200
committerGaëtan Gilbert2019-09-24 14:53:04 +0200
commit90553b5ca20f2acc9803baf0cf487eb34b6c8f12 (patch)
treea6e06854ad02f9106ca88b00c37588535e12b563
parent35c997c5c2ab6ee2f29fbeb548359e63c23a1394 (diff)
parent7b59d8c9d9b2104de7162ec0e40f6182a6830046 (diff)
Merge PR #10699: [gitlab/ci] Prevent Corn from running if Bignums has failed.
Reviewed-by: SkySkimmer
-rw-r--r--.gitlab-ci.yml8
1 files changed, 6 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 64d930a735..8b37403960 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -8,8 +8,11 @@ stages:
- stage-4 # Only dependencies in stage 1, 2 and 3
- deploy
-# When a job has no dependencies, it goes to stage 1.
-# Otherwise, we set "needs" and "dependencies" to the same value.
+# When a job has no dependencies, it goes to stage 1. Otherwise, we
+# set both "needs" and "dependencies". "needs" is a superset of
+# "dependencies" that should include all the transitive dependencies.
+# "dependencies" only list the previous jobs whose artifact we need to
+# keep.
# some default values
variables:
@@ -657,6 +660,7 @@ library:ci-corn:
stage: stage-4
needs:
- build:edge+flambda
+ - plugin:ci-bignums
- library:ci-math-classes
dependencies:
- build:edge+flambda