From 95d977bf0b1825b7d822abbdd062cdb8c38051cb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 22 Jan 2019 23:29:28 +0100
Subject: Remove travis

The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
---
 CONTRIBUTING.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CONTRIBUTING.md')

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index de7fb9183c..bb0e388cdd 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -55,7 +55,7 @@ please add an entry to [`dev/doc/critical-bugs`](/dev/doc/critical-bugs).
 
 Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes.
 
-Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`.
+Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by the `lint` job on GitLab CI (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`.
 
 Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests.
 
-- 
cgit v1.2.3