| name: docs |
| on: |
| # For manual pushes. |
| workflow_dispatch: |
| |
| # Pushes to main that touch the documentation directory. |
| push: |
| branches: |
| - master |
| paths: |
| - 'docs/**' |
| |
| permissions: |
| contents: write |
| jobs: |
| deploy: |
| runs-on: ubuntu-latest |
| steps: |
| - uses: actions/checkout@v4 |
| - name: Configure Git Credentials |
| run: | |
| git config user.name github-actions[bot] |
| git config user.email 41898282+github-actions[bot]@users.noreply.github.com |
| - uses: actions/setup-python@v5 |
| with: |
| python-version: 3.x |
| - run: echo "cache_id=$(date --utc '+%V')" >> $GITHUB_ENV |
| - uses: actions/cache@v4 |
| with: |
| key: mkdocs-material-${{ env.cache_id }} |
| path: .cache |
| restore-keys: | |
| mkdocs-material- |
| - run: pip install mkdocs-material |
| - run: pip install mkdocs-redirects |
| - run: mkdocs gh-deploy --force -f docs/mkdocs.yml |