diff options
| author | Gaëtan Gilbert | 2019-01-22 23:29:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-22 23:32:46 +0100 |
| commit | 95d977bf0b1825b7d822abbdd062cdb8c38051cb (patch) | |
| tree | 930521bfe8d77d5fc11e42d562ea6607cdfe81ec /dev/ci/README-developers.md | |
| parent | 03c17218eeacb098ff57ecee1d98f46b7c8fa185 (diff) | |
Remove travis
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
Diffstat (limited to 'dev/ci/README-developers.md')
| -rw-r--r-- | dev/ci/README-developers.md | 6 |
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: |