| name: Deploy GitHub Pages | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'docs/**' | |
| - 'scripts/publish_gh_pages.sh' | |
| - '.github/workflows/deploy-pages.yml' | |
| workflow_dispatch: | |
| permissions: | |
| contents: write | |
| jobs: | |
| deploy: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Configure git identity | |
| run: | | |
| git config user.email "41898282+github-actions[bot]@users.noreply.github.com" | |
| git config user.name "github-actions[bot]" | |
| - name: Publish docs to gh-pages | |
| run: bash scripts/publish_gh_pages.sh | |