diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-06 19:25:16 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-06 19:25:16 +0200 |
| commit | 6748d06e9618a91a63cd09b4809e67b665818acd (patch) | |
| tree | 9b1440c74ea119f2c46545bb282628f14ed773c8 | |
| parent | b493c2b9c8dfcadb3aee37a7b98052e611bb00a2 (diff) | |
| parent | 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d (diff) | |
Merge PR #7721: Add a note about [ci skip] in CI README.
| -rw-r--r-- | dev/ci/README.md | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 697a160ca..dc586c61f 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -89,6 +89,11 @@ 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: |