deploy_documentation.yml

on:
  release:
    types: [published]
  workflow_run:
    workflows:
      - Release
    types:
      - completed
  pull_request:
    types: [labeled]

name: Deploy documentation for latest release
jobs:
  deploy_documentation:
    if: ${{ github.event.action == 'completed' || github.event.label.name == 'test-release-process' || (github.event_name == 'release' && github.event.action == 'published') }}
    runs-on: ubuntu-latest
    steps:
      - name: Checkout
        uses: actions/checkout@v1
      - name: Get the release version from the GITHUB_REF variable as new SHORT_VERSION variable
        run: echo "SHORT_VERSION=$(echo ${GITHUB_REF} | sed -E 's/^refs\/heads\/.*/develop/' | sed -E 's/^(refs\/tags\/v)?(.*)(\.[0-9]+\.[0-9]+)$/\2/')" >> $GITHUB_ENV
      - run: misc/download-mdbook.sh 0.4.52
        env:
          OS_NAME: linux
      - name: Generate the documentation
        run: mdbook build --dest-dir book/v${SHORT_VERSION} docs/
      - run: git clone -q  -b gh-pages https://github.com/$GITHUB_REPOSITORY gh-pages
      - name: Remove old files for this version
        run: rm -Rf gh-pages/docs/v$SHORT_VERSION
      - name: copy the documentation content
        run: cp -R docs/book/* gh-pages/docs/
      - run: git add docs/v$SHORT_VERSION
        working-directory: gh-pages
      - run: git -c user.name='gh-actions' -c user.email='gh-actions' commit --allow-empty -m "add documentation for version $SHORT_VERSION"
        working-directory: gh-pages
      - name: Push changes
        uses: ad-m/github-push-action@v0.6.0
        with:
          github_token: ${{ secrets.GITHUB_TOKEN }}
          directory: gh-pages
          branch: gh-pages