aboutsummaryrefslogtreecommitdiff
path: root/dev/lint-repository.sh
AgeCommit message (Collapse)Author
2019-02-18Fix per-commit linting with bot mergesGaëtan Gilbert
When the bot auto-merged the linter saw no commits to lint, eg https://gitlab.com/coq/coq/-/jobs/162893603 I'm pushing from a non-current master so we will see if this works.
2018-12-21Move lint job to gitlabGaëtan Gilbert
This changes the semantics a bit since we don't have TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the commits since the last merge commit.
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
We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
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
We use git check-attr to look at the same files as git diff --check.