diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2019-11-19 10:56:42 +0100 |
|---|---|---|
| committer | Rémi Verschelde <rverschelde@gmail.com> | 2019-11-19 12:14:46 +0100 |
| commit | 95f1f4e82a948f064bbbe32812a3f4b5c3c90bb7 (patch) | |
| tree | 40d6ef97efea8bbb1256ae7d1c60e40947e0e94b /core/set.h | |
| parent | 7a0228fbbabe93a5e49f9b40410969f5de99d25c (diff) | |
Travis: Drop support for coverity_scan, we do not use it
The UX is pretty bad, and the fact that all reports are private by
default with no option to make them public makes Coverity Scan hardly
usable in a community-driven project.
Diffstat (limited to 'core/set.h')
0 files changed, 0 insertions, 0 deletions