Chore: Update DevOps tooling from central repository [skip ci] #224

	---
	name: "📘 Documentation build/publish"

	# yamllint disable-line rule:truthy
	on:
	workflow_dispatch:
	pull_request:
	types: [closed]
	branches:
	- "*"
	- "!update-devops-tooling"

	jobs:
	build_and_deploy:
	# Only run when pull request is merged
	if: github.event.pull_request.merged == true
	name: "Rebuild documentation"
	runs-on: ubuntu-latest
	continue-on-error: true

	permissions:
	# IMPORTANT: mandatory for documentation updates; used in final step
	id-token: write
	pull-requests: write
	contents: write
	repository-projects: write

	steps:
	- name: "Checkout repository"
	uses: actions/checkout@v4

	- name: "Set up Python"
	uses: actions/setup-python@v5
	with:
	python-version: "3.11"

	- name: "Setup PDM for build commands"
	uses: pdm-project/setup-pdm@v4

	- name: "Install dependencies"
	run: \|
	python -m pip install --upgrade pip
	pdm lock
	pdm export -o requirements.txt
	if [ -f docs/requirements.txt ]; then
	pip install -r docs/requirements.txt; fi

	- name: "Build documentation: (tox/sphinx)"
	run: \|
	pip install --upgrade tox
	tox -e docs

	- name: "Publish documentation"
	if: success()
	uses: peaceiris/actions-gh-pages@v4
	with:
	publish_branch: gh-pages
	github_token: ${{ secrets.GITHUB_TOKEN }}
	publish_dir: docs/_build/html/
	keep_files: true

Provide feedback