.github/workflows/docs.yml

# Update the API documentation whenever the `main` branch changes.
# This documentation lives in its own `docs` branch.
name: docs

on:
  push:
    branches:
      - 'main'

jobs:
  update-docs-branch:
    runs-on: ubuntu-20.04 # latest
    permissions:
      contents: write # allow push
    steps:
      - name: Checkout
        uses: actions/checkout@v3
        with:
          submodules: true

      - name: Update docs branch
        run: |
          ./make-docs.sh

      - name: Commit
        run: |
          git config --local user.email "action@github.com"
          git config --local user.name "GitHub Action"
          git add --force docs/
          git commit --message="update docs"

      - name: Push to docs branch
        uses: ad-m/github-push-action@v0.6.0
        with:
          github_token: ${{ github.token }}
          branch: docs
          # Force push so that `docs` branch always looks like `main`,
          # but with 1 additional "update docs" commit.
          # This seems simpler than trying to cleanly merge `main` into
          # `docs` each time.
          force: true