aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/README-developers.md
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci/README-developers.md')
-rw-r--r--dev/ci/README-developers.md6
1 files changed, 2 insertions, 4 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6663fbecf8..10b4f9b044 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,14 +16,12 @@ We are currently running tests on the following platforms:
`./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.
-
- AppVeyor is used to test the compilation of Coq and run the test-suite on
Windows.
- Azure Pipelines is used to test the compilation of Coq and run the
- test-suite on Windows. It is expected to replace appveyor eventually.
+ test-suite on Windows and on macOS. It is expected to replace
+ appveyor eventually.
You can anticipate the results of most of these tests prior to submitting your
PR by running GitLab CI on your private branches. To do so follow these steps: