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.
---
 dev/doc/MERGING.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/doc/MERGING.md')

diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 56fdab0c26..5705857d76 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -93,7 +93,7 @@ put the approriate label. Otherwise, they are expected to merge the PR using the
 
 When CI has a few failures which look spurious, restarting the corresponding
 jobs is a good way of ensuring this was indeed the case.
-To restart a job on Travis or on AppVeyor, you should connect using your GitHub
+To restart a job on AppVeyor, you should connect using your GitHub
 account; being part of the Coq organization on GitHub should give you the
 permission to do so.
 To restart a job on GitLab CI, you should sign into GitLab (this can be done
-- 
cgit v1.2.3