Merge branch 'main' into docs-touchup #568

	name: GitHub Pages

	on: # Always attempt html build on push & PR, but only deploy when there is a new tag.
	push:
	branches:
	- main
	tags:
	- v*
	pull_request:
	branches:
	- main
	workflow_dispatch: # Allows to manually trigger the job from the web UI.

	jobs:
	build:
	name: Build documentation (and deploy for git tag)
	runs-on: ubuntu-latest
	permissions:
	contents: write
	concurrency:
	group: ${{ github.workflow }}-${{ github.ref }}
	steps:
	- name: Checkout repository
	uses: actions/checkout@v4

	- name: Setup Python
	uses: actions/setup-python@v5
	with:
	python-version: '3.12'

	- name: Build
	uses: extractions/setup-just@v1
	run: \|
	sudo apt-get update
	sudo apt-get install -y python3-pip
	python3 -m pip install --upgrade pip
	python3 -m venv .venv-gh-pages
	source .venv-gh-pages/bin/activate
	python3 -m pip install "$PWD"[doc,test]
	just html
	- name: Deploy
	uses: peaceiris/actions-gh-pages@v4
	if: ${{ startsWith(github.ref, 'refs/tags/') }}
	with:
	github_token: ${{ secrets.GITHUB_TOKEN }}
	publish_dir: ./html

Provide feedback