diff options
| author | Théo Zimmermann | 2019-08-24 08:50:43 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-24 08:51:11 +0200 |
| commit | 7b59d8c9d9b2104de7162ec0e40f6182a6830046 (patch) | |
| tree | 10f3bfc0ea33c9143f86d40bdc1fae5b73f61920 /plugins/syntax | |
| parent | 07c4c8cac353883a2c6ae493556b9b544f3f38c0 (diff) | |
[gitlab/ci] Prevent Corn from running if Bignums has failed.
The needs keyword needs to include all the transitive dependencies.
Otherwise, we risk stage-3 being skipped but stage-4 being run as in
https://gitlab.com/coq/coq/pipelines/78119475.
The reason why we don't need to include bignums in the dependencies of
corn is because the artifact for math-classes is the directory where
both bignums and math-classes were built.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions