Merge remote-tracking branch 'origin/develop' into develop #104

	name: Documenation

	on:
	pull_request:
	types:
	- opened
	- synchronize
	- reopened
	- ready_for_review
	branches:
	- master
	- develop
	push:
	branches:
	- develop

	jobs:
	test-docstrings:
	# do not trigger on draft PRs
	if: ${{ ! github.event.pull_request.draft }}
	runs-on: ubuntu-24.04
	steps:
	- name: Check out repository
	uses: actions/checkout@v4

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

	- name: Upgrade pip
	run: python3 -m pip install --upgrade pip

	- name: Install dependencies
	run: pip install -qU pydocstyle

	- name: Check docstrings
	# Ignoring the cached_properties because pydocstyle (sometimes?) treats them as functions.
	run: pydocstyle --convention=numpy mala

	build-and-deploy-pages:
	needs: test-docstrings
	runs-on: ubuntu-24.04
	steps:
	- name: Check out repository
	uses: actions/checkout@v4
	with:
	fetch-depth: 0 # 0 fetches complete history and tags

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

	- name: Upgrade pip
	run: python3 -m pip install --upgrade pip

	- name: Install dependencies
	run: \|
	pip install -r docs/requirements.txt

	- name: Build API and docs
	run: \|
	make -C docs apidocs
	sphinx-build -W --keep-going -b html -d docs/_build/doctrees docs/source docs/_build/html
	mv -v docs/_build/html public

	- name: Deploy
	if: ${{ github.event_name == 'push' }}
	uses: peaceiris/actions-gh-pages@v3
	with:
	deploy_key: ${{ secrets.ACTIONS_DEPLOY_KEY }}
	publish_dir: ./public

Provide feedback