diff options
| author | Maxime Dénès | 2018-02-28 09:58:29 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-28 09:58:29 +0100 |
| commit | aec08b873425f6cdae4e1434651b4e9a97d0ced0 (patch) | |
| tree | 429154521843b881bf393b102b1e4af6b57d5d23 /kernel | |
| parent | e3124e098ef8170dac2b348b91757a7034bc4999 (diff) | |
| parent | 05ad387ae689e6b95d31d62205e25c736cf52864 (diff) | |
Merge PR #6752: Remove from CircleCI builds that are already taken care of by Travis.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions