diff options
| author | Gaëtan Gilbert | 2018-12-14 15:19:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-21 15:33:36 +0100 |
| commit | b80e0b73e4417f414d723cfb2f424ecec321767d (patch) | |
| tree | 6530c90fe39592bac554bfdb588bee60ebd43de2 /dev/ci/README-developers.md | |
| parent | ee98d818791d8f92674934cda02bfcb3667013c9 (diff) | |
Move lint job to gitlab
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.
Diffstat (limited to 'dev/ci/README-developers.md')
| -rw-r--r-- | dev/ci/README-developers.md | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index fa8962a06f..6663fbecf8 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -10,12 +10,14 @@ We are currently running tests on the following platforms: - GitLab CI is the main CI platform. It tests the compilation of Coq, of the documentation, and of CoqIDE on Linux with several versions of OCaml and with warnings as errors; it runs the test-suite and - tests the compilation of several external developments. + tests the compilation of several external developments. It also runs + a linter that checks whitespace discipline. A [pre-commit + hook](../tools/pre-commit) is automatically installed by + `./configure`. It should allow complying with this discipline + without pain. - Travis CI is used to test the compilation of Coq and run the test-suite on - macOS. It also runs a linter that checks whitespace discipline. A - [pre-commit hook](../tools/pre-commit) is automatically installed by - `./configure`. It should allow complying with this discipline without pain. + macOS. - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. |