diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml new file mode 100644 index 0000000..9b8921d --- /dev/null +++ b/.github/workflows/pages.yml @@ -0,0 +1,40 @@ +name: Pages + +# Regenerates the docs site from docs/WIKI.md and publishes it to GitHub Pages. +on: + push: + branches: [main] + paths: + - "docs/**" + - "scripts/build_site.py" + - ".github/workflows/pages.yml" + workflow_dispatch: + +permissions: + contents: read + pages: write + id-token: write + +concurrency: + group: pages + cancel-in-progress: false + +jobs: + deploy: + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: "3.x" + - name: Build the site + run: python3 scripts/build_site.py + - uses: actions/configure-pages@v5 + - uses: actions/upload-pages-artifact@v3 + with: + path: site + - id: deployment + uses: actions/deploy-pages@v4