diff options
| author | Gaëtan Gilbert | 2020-07-20 11:04:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-20 11:04:21 +0200 |
| commit | 3039bb02e0029b771cc904a5806b5cb8f99d6c49 (patch) | |
| tree | 8f115c46afe74e4108cde9a3a060ed0c2584f029 /.gitlab-ci.yml | |
| parent | d6aff7758936e4028614a1ac7e1dfbc5c7f82076 (diff) | |
CI: deploy make-built stdlib doc
Workaround #12699
Alternative to #12700
Diffstat (limited to '.gitlab-ci.yml')
| -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" |