deploy_development_docs.yml

name: deploy development docs
on:
  push:
    branches: [main]

jobs:
  build:
    name: Deploy development docs
    if: "!contains(github.repository, '-insiders/')"
    runs-on: ubuntu-latest
    steps:
    - name: Checkout main
      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2

    - name: Set up documentation mutex
      uses: suzuki-shunsuke/lock-action@latest
      with:
        mode: lock
        key: docs-lock
        post_unlock: 'true'
        remove_key_when_unlock: 'true'
        max_wait_seconds: '500'
        wait_interval_seconds: '50'

    - run: pip install hatch
    - name: publish docs
      env:
        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
      run: |
        git config user.name "Frank Hoffmann"
        git config user.email "15r10nk@users.noreply.github.com"
        git fetch origin gh-pages --depth=1
        hatch run docs:mike deploy --push development