diff options
| author | Théo Zimmermann | 2018-08-01 14:09:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-01 14:10:24 +0200 |
| commit | e348f5475a3cb4c7078a4fb8cc9c60c0fd6fff13 (patch) | |
| tree | 0d244be6742bb597f48f9b1e574f493a763736b4 /dev/ci | |
| parent | 3a726a733a0d4c7ea3db30e71829ca27eab1776a (diff) | |
Update documentation on GitLab CI to reflect recent changes.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README.md | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 43d680af61..a814e4914e 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -138,14 +138,11 @@ persists to and is used by the next jobs. Artifacts can also be downloaded from the GitLab repository. Currently, available artifacts are: -- the Coq executables and stdlib, in three copies varying in +- the Coq executables and stdlib, in four copies varying in architecture and OCaml version used to build Coq. -- the Coq documentation, built only in the `build:base` job. When submitting +- the Coq documentation, built in the `documentation` job. When submitting a documentation PR, this can help reviewers checking the rendered result. -As an exception to the above, jobs testing that compilation triggers -no OCaml warnings build Coq in parallel with other tests. - ### GitLab and Windows If your repository has access to runners tagged `windows`, setting the |