diff options
| author | Théo Zimmermann | 2018-06-22 09:15:41 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-06-22 09:16:15 +0200 |
| commit | 90aa46819c8f0c4ed2813f69ddfe4b65708135be (patch) | |
| tree | 72807abab52bb5f92dd81572ae5885e7ac1eec97 /dev | |
| parent | df35025b2be4a0dc9aadecc0e3110a21012683cf (diff) | |
Revert "Add a note about [ci skip] in CI README."
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/README.md | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 08364c897a..45176581cd 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -86,11 +86,6 @@ We are currently running tests on the following platforms: - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. -GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit -message to bypass CI. Do not use this unless your commit only changes files -that are not compiled (e.g. Markdown files like this one, or files under -[`.github/`](../../.github/)). - 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: |