diff options
| author | Emilio Jesus Gallego Arias | 2020-07-20 15:47:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-20 15:47:26 +0200 |
| commit | f44202e28f38aa900801b0c90514690b6a401bed (patch) | |
| tree | 61f7e840cc45e9650c2a1462553222bd791286ea | |
| parent | d57839d4fa3f7611b961bf28773b2969b659b24b (diff) | |
| parent | 3039bb02e0029b771cc904a5806b5cb8f99d6c49 (diff) | |
Merge PR #12712: CI: deploy make-built stdlib doc
Reviewed-by: ejgallego
| -rw-r--r-- | .gitlab-ci.yml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3b95800f0d..ec8fe23171 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -481,6 +481,8 @@ doc:refman-pdf:dune: - _build/log - _build/default/doc/refman-pdf +# currently bugged: dune cleans up the glob files so no links +# see #12699 doc:stdlib:dune: extends: .dune-ci-template variables: @@ -501,11 +503,11 @@ doc:refman:deploy: dependencies: - doc:ml-api:odoc - doc:refman:dune - - doc:stdlib:dune + - build:base needs: - doc:ml-api:odoc - doc:refman:dune - - doc:stdlib:dune + - build:base script: - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy @@ -515,7 +517,7 @@ doc:refman:deploy: - mkdir -p _deploy/$CI_COMMIT_REF_NAME - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api - cp -rv _build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman - - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib + - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib - cd _deploy/$CI_COMMIT_REF_NAME/ - git add api refman stdlib - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA" |