publish_doc.yml

name: Publish documentation

on:
  push:
    branches:
      - main
  pull_request:
    paths:
      - 'docs/**'
  workflow_dispatch:

permissions:
  contents: write

jobs:
  deploy:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3
      - uses: actions/setup-python@v4
        with:
          python-version: '3.7'
      - name: Cap pip version
        run: pip install -U "pip<23"
      - run: pip install .[doc]
      - name: Set up Git
        run: |
          git config user.name ${{ github.actor }}
          git config user.email ${{ github.actor }}@users.noreply.github.com
      - name: Delete existing doc
        run: |
          git fetch origin gh-pages
          mike delete ${{ github.head_ref }}
        continue-on-error: true
      - name: Deploy main
        if: github.event_name == 'push'
        run: |
          git fetch origin gh-pages
          mike delete main
          mike deploy --push main
      - name: Deploy branch
        if: github.event_name == 'pull_request'
        run: |
          git fetch origin gh-pages
          mike deploy --push ${{ github.head_ref }}