Commit graph

1 commit

Author SHA1 Message Date
Zbigniew Jędrzejewski-Szmek 748c59b110 Rename scripts/coverity.sh to tools/coverity.sh
There are only two files in tools/, I don't think we need a separate
directory for them.
2018-03-12 15:39:21 +01:00
Renamed from scripts/coverity.sh (Browse further)