diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README.md | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 2 |
2 files changed, 1 insertions, 6 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 08364c897..45176581c 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: diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87d837b38..3807ff90c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -119,7 +119,7 @@ ######################################################################## # coq-dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}" +: "${coq_dpdgraph_CI_BRANCH:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" ######################################################################## |