aboutsummaryrefslogtreecommitdiff
path: root/dev/lint-repository.sh
AgeCommit message (Expand)Author
2019-02-18Fix per-commit linting with bot mergesGaëtan Gilbert
2018-12-21Move lint job to gitlabGaëtan Gilbert
2018-03-31Linter: verify overlay extensions.Gaëtan Gilbert
2018-02-08Fix redirection to stderr in lint-repository error message.Gaëtan Gilbert
2018-01-16Simplify logic and streamline lint-repository.shGaëtan Gilbert
2018-01-08Cleanup conditional in lint-repository.shGaëtan Gilbert
2017-12-06Linter: skip PRs older than the linter.Gaëtan Gilbert
2017-10-25Linter: check that files end with newlines.Gaëtan Gilbert