diff options
| author | Vincent Laporte | 2019-02-05 10:37:21 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-06 22:59:45 +0000 |
| commit | 1e91dc506a3b9bad4208bab1e4d05e692638c67e (patch) | |
| tree | 82ede900a10e18077195d68154be1e0f5846fac3 | |
| parent | 7886c6d8e0663ba346fff52837012c7fc952ecc1 (diff) | |
[Gitlab-CI] Deploy manual to GH-Pages
| -rw-r--r-- | .gitlab-ci.yml | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7ebc2d8a4d..623debea23 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -4,6 +4,7 @@ stages: - docker - build - test + - deploy # some default values variables: @@ -347,6 +348,35 @@ doc:refman:dune: paths: - _build/default/doc/sphinx_build/html +doc:refman:deploy: + stage: deploy + environment: + name: deployment + url: https://coq.github.io/ + only: + variables: + - $DOCUMENTATION_DEPLOY_KEY + dependencies: + - doc:refman:dune + before_script: + - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) + - eval $(ssh-agent -s) + - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null + - mkdir -p ~/.ssh + - chmod 700 ~/.ssh + - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts + - git config --global user.name "coqbot" + - 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 + - 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" + - git push # TODO: rebase and retry on failure + doc:ml-api:odoc: <<: *dune-ci-template variables: |