diff options
| author | Emilio Jesus Gallego Arias | 2018-05-14 04:20:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-14 04:22:39 +0200 |
| commit | 6bf8018c3d1fdfff974d0e83913bb3a42281b01e (patch) | |
| tree | b6744b2a4a34c4c850c26c7a05d670977daa7270 /dev/ci/ci-basic-overlay.sh | |
| parent | 12109393c957ef64f7dc8d47b745a75392e4382c (diff) | |
[ci] [circleci] Remove jobs done in Gitlab efficiently.
Following the migration to Gitlab (#6919) we reduce Circle load, see
also discussion in #7436 and #7482.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions