name: Release Docs

on:
  push:
    tags:
      - "v*"
  # See https://docs.github.com/fr/webhooks/webhook-events-and-payloads#workflow_dispatch
  # Can be used to update doc with latest tag
  workflow_dispatch:

permissions: {}

jobs:
  release_docs:
    permissions:
      contents: write  #  for mike to push

    name: Release Docs
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
        with:
          fetch-depth: 0

      - uses: actions/setup-python@e797f83bcb11b83ae66e0230d6156d7c80228e7c # v6.0.0
        with:
          python-version: "3.12"
          cache: "pip"
          cache-dependency-path: "./docs/scripts/requirements.txt"

      - run: |
          pip install -r docs/scripts/requirements.txt

      - name: Configure Git user
        run: |
          git config --local user.email "github-actions[bot]@users.noreply.github.com"
          git config --local user.name "github-actions[bot]"

      - name: build and push
        run: |
          VERSION="${{ github.ref_name }}"
          if [[ ${{ github.event_name }} == "workflow_dispatch" ]]; then
            VERSION="latest"
          fi
          mike deploy $VERSION --push --update-aliases
          mike set-default --push latest