aboutsummaryrefslogtreecommitdiff
path: root/dev/lint-repository.sh
AgeCommit message (Expand)Author
2020-11-26CI: Use hash of dockerfile in CACHEKEYGaëtan Gilbert
2020-11-24Fix linter: incorrect commit was picked in CIGaëtan Gilbert
2020-09-28Remove the linter ocamlformat pass.Pierre-Marie Pédrot
2020-01-22[lint] Use makefile wrapper instead of calling dune command directly.Emilio Jesus Gallego Arias
2019-12-13[fmt] [dune] Add ocamlformat configuration.Emilio Jesus Gallego Arias
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