diff options
| author | Emilio Jesus Gallego Arias | 2020-03-22 00:30:25 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-22 00:30:25 -0400 |
| commit | ec4b889aa4e837bd82a7d0a059d0c967cde1ac46 (patch) | |
| tree | b0945180cd3501e463f1804e12d06a13aed1fa60 /.gitlab-ci.yml | |
| parent | 4d025d4161599ea20cd1dbf489a6412f019a7a7e (diff) | |
| parent | 80f3011eb5ca479b9b1f059c0f04e131028d5312 (diff) | |
Merge PR #11855: Build and install refman with Dune.
Ack-by: SkySkimmer
Reviewed-by: ejgallego
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 |