diff options
| author | Emilio Jesus Gallego Arias | 2018-08-20 17:31:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-08-20 17:31:54 +0200 |
| commit | 449c9384f93c5af82d58baf280c7c17accee86d2 (patch) | |
| tree | 189f97462ae7f4e88fe922d08d7ee1230a856a8a /dev | |
| parent | b393d91c0f628f0687486fb2d321f262981a4d33 (diff) | |
| parent | e348f5475a3cb4c7078a4fb8cc9c60c0fd6fff13 (diff) | |
Merge PR #8258: Update documentation on GitLab CI to reflect recent changes.
Diffstat (limited to 'dev')
| -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 |