diff options
| author | Gaëtan Gilbert | 2018-05-16 13:16:05 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-16 13:16:05 +0200 |
| commit | 3f480c993311d19b152deb6bb4dc561188d76fc7 (patch) | |
| tree | 289b97e8d9a7636771c5f624601bf968d897f721 /Makefile.common | |
| parent | 768883a6b7002bcdc589b43c199b2c0b1d2c23b5 (diff) | |
| parent | dce5566785a313b0e20bc183dbfd7e2aa7499b53 (diff) | |
Merge PR #7436: [travis] Remove some more jobs from PR testing now that they are on Gitlab.
Diffstat (limited to 'Makefile.common')
0 files changed, 0 insertions, 0 deletions