aboutsummaryrefslogtreecommitdiff
path: root/ci/extended_lint
AgeCommit message (Expand)Author
2019-11-21ci: Remove unmaintained extended_lintMarcoFalke
2019-08-15ci: Rename .travis/ to ./ci/MarcoFalke