diff options
| author | Théo Zimmermann | 2019-08-23 17:44:28 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-23 17:44:28 +0200 |
| commit | a580f0f072e614b4713b91ae1e033fed7e20f053 (patch) | |
| tree | cb1152b47a181d991c00d6e1e7a194bc0a86ae69 /kernel/dune | |
| parent | 0fc73b31859abb42f3fccf018497b33dfa49c33b (diff) | |
[gitlab/ci] Rework stages, always use needs keyword.
Now everything that does not have any dependencies goes to the first stage.
The rest goes to the first stage following all its dependencies.
All jobs specifying a dependencies keyword also specify a needs keyword.
Diffstat (limited to 'kernel/dune')
0 files changed, 0 insertions, 0 deletions
