diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4a053ec03f..5b343a23c5 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -426,7 +426,16 @@ doc:refman:dune: artifacts: paths: - _build/log - - _build/default/doc/sphinx_build/html + - _build/default/doc/refman-html + +doc:refman-pdf:dune: + extends: .dune-ci-template + variables: + DUNE_TARGET: refman-pdf + artifacts: + paths: + - _build/log + - _build/default/doc/refman-pdf doc:stdlib:dune: extends: .dune-ci-template |