diff options
| author | Gaëtan Gilbert | 2019-02-07 15:14:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-07 15:14:21 +0100 |
| commit | 99c1d7b0ae1beed66fe8dd6a06db84dc0c8322d8 (patch) | |
| tree | b53dcab9d7ab26efbfb469d41d5a7d05ab47ff09 | |
| parent | d1538ff126a19b7b5f9a2a95a0175d8d6ac71e39 (diff) | |
| parent | 1e91dc506a3b9bad4208bab1e4d05e692638c67e (diff) | |
Merge PR #9475: Automatic deployment of the user manual to GH-Pages
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: vbgl
| -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: |