diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-05 17:58:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-05 17:58:39 +0200 |
| commit | caacdb00c830854de72ba2fe19b5f74951d445bf (patch) | |
| tree | a90fb194c2f00274fec0f3eeaba5ae30d6d0573c /tools | |
| parent | 3ded029b42c7acf0b1b575cf4f0bb395a1d0d823 (diff) | |
| parent | 56001961201e3092005cd898151c8ba4b798b6ed (diff) | |
Merge PR #7991: Make Travis faster by removing more builds.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions