From b80e0b73e4417f414d723cfb2f424ecec321767d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Dec 2018 15:19:19 +0100
Subject: 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.
---
 dev/ci/README-developers.md | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'dev/ci')

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.
-- 
cgit v1.2.3