diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/README-developers.md | 6 | ||||
| -rw-r--r-- | dev/ci/README-users.md | 2 | ||||
| -rw-r--r-- | dev/ci/README.md | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 54da7a7cd3..6ca3aa2981 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -1,7 +1,7 @@ Information for developers about the CI system ---------------------------------------------- -When you submit a pull request (PR) on Coq GitHub repository, this will +When you submit a pull request (PR) on the Coq GitHub repository, this will automatically launch a battery of CI tests. The PR will not be integrated unless these tests pass. @@ -76,7 +76,7 @@ above steps. In order to do so, call the script as: ``` ./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac ``` -replacing `ejgallego` by your github id and `9873` by the actual PR +replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR number. The script will: - checkout the contributions and prepare the branch/remote so you can @@ -86,7 +86,7 @@ number. The script will: For problems related to ML-plugins, if you use `dune build` to build Coq, it will actually be aware of the broken contributions and perform a global build. This is very convenient when using `merlin` as you -will get a coherent view of all the broken plugins, which full +will get a coherent view of all the broken plugins, with full incremental cross-project rebuild. Advanced GitLab CI information diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index f606f43fd5..01769aeddb 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -76,7 +76,7 @@ developer commands work more seamlessly. ### Supported CI images for Coq -The Coq developers and contributors do provide official Docker and Nix +The Coq developers and contributors provide official Docker and Nix images for testing against Coq master. Using these images is highly recommended: diff --git a/dev/ci/README.md b/dev/ci/README.md index 9eb86c7f07..afbfab3ac6 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -6,7 +6,7 @@ breakage on our Continuous Integration (CI) platforms *before* integration, so as to ensure better robustness and catch problems as early as possible. These tests include the compilation of several external libraries / plugins. -This README is split on two specific documents: +This README is split into two specific documents: - [README-users.md](./README-users.md) which contains information for authors of external libraries and plugins who might be interested in |