diff options
| author | Emilio Jesus Gallego Arias | 2018-12-27 09:16:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-27 09:16:21 +0100 |
| commit | 721457e41db164057025f48a8a46596397c0c5c8 (patch) | |
| tree | 10044730266bf752cf15f96be0803d4ed405501b /dev/ci | |
| parent | 86fc5bbbd93f7e6c380bc3a9a4271fc83214264d (diff) | |
| parent | b80e0b73e4417f414d723cfb2f424ecec321767d (diff) | |
Merge PR #9224: Move lint job to gitlab
Diffstat (limited to 'dev/ci')
| -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. |