diff options
| author | Emilio Jesus Gallego Arias | 2019-02-08 09:49:31 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-08 09:49:31 +0100 |
| commit | 79b6317f738b6d2d7fdaaaad2cef79a092ec8c77 (patch) | |
| tree | 399c6aff17fe7cd94453b09a31c3977b1aaa5a57 | |
| parent | a2365c54ea7cdaa8a20f43c9f46d7bfef6e1180a (diff) | |
| parent | ef8a8ce0d502aea57c5f630fb6edc123166cad4e (diff) | |
Merge PR #9515: [Gitlab-CI] Automatic deployment of the standard library documentation to GH-pages
Reviewed-by: ejgallego
| -rw-r--r-- | .gitlab-ci.yml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index aef51d8ac0..fac5abf13f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -357,7 +357,7 @@ doc:refman:deploy: variables: - $DOCUMENTATION_DEPLOY_KEY dependencies: - - doc:refman:dune + - doc:refman before_script: - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) - eval $(ssh-agent -s) @@ -369,12 +369,14 @@ doc:refman:deploy: - git config --global user.email "coqbot@users.noreply.github.com" script: - git clone git@github.com:coq/doc.git _deploy - - rm -rf _deploy/$CI_COMMIT_REF_NAME/refman # NB: won’t work if branch name has ‘/’ in it + - rm -rf _deploy/$CI_COMMIT_REF_NAME/refman + - rm -rf _deploy/$CI_COMMIT_REF_NAME/stdlib - mkdir -p _deploy/$CI_COMMIT_REF_NAME - - cp -rv _build/default/doc/sphinx_build/html _deploy/$CI_COMMIT_REF_NAME/refman - - cd _deploy/$CI_COMMIT_REF_NAME/refman - - git add . - - git commit -m "User manual of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA" + - cp -rv _install_ci/share/doc/coq/sphinx/html _deploy/$CI_COMMIT_REF_NAME/refman + - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib + - cd _deploy/$CI_COMMIT_REF_NAME/ + - git add refman stdlib + - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA" - git push # TODO: rebase and retry on failure doc:ml-api:odoc: |