diff options
author | 2018-05-14 04:20:26 +0200 | |
---|---|---|
committer | 2018-05-14 04:22:39 +0200 | |
commit | 6bf8018c3d1fdfff974d0e83913bb3a42281b01e (patch) | |
tree | b6744b2a4a34c4c850c26c7a05d670977daa7270 /theories/Setoids | |
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 'theories/Setoids')
0 files changed, 0 insertions, 0 deletions