diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-10 18:34:44 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-10 18:34:44 +0200 |
commit | b4572185522cd21e7e4e1cf59095ae66d0da0be1 (patch) | |
tree | 37803edada0dcd5b8c543c322c1839801b9e254d /test-suite/failure/cases.v | |
parent | da13cd2f7bf29be080922dcf07f1fc6a9d4cb4ec (diff) | |
parent | 6964772d33a7ee10c28b6f07767c0e391b7dd123 (diff) |
Merge PR #8036: [travis] Remove even more jobs.
Diffstat (limited to 'test-suite/failure/cases.v')
0 files changed, 0 insertions, 0 deletions