From e348f5475a3cb4c7078a4fb8cc9c60c0fd6fff13 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 1 Aug 2018 14:09:57 +0200 Subject: Update documentation on GitLab CI to reflect recent changes. --- dev/ci/README.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'dev') 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 -- cgit v1.2.3