Update changelog #72

	name: Build docs
	permissions:
	contents: write
	on:
	workflow_dispatch:
	push:
	branches:
	- "main"
	# - "rel-v[0-9]+.[0-9]+"
	# - "rel-v[0-9]+.[0-9]+.[0-9]+"
	tags:
	- "v[0-9]+.[0-9]+.[0-9]+"

	jobs:
	deploy:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout sources
	uses: actions/checkout@v4

	- name: Configure Git Credentials
	run: \|
	git config user.name github-actions[bot]
	git config user.email github-actions[bot]@users.noreply.github.com

	- name: Setup Python
	uses: actions/setup-python@v5
	with:
	python-version: 3.x

	- name: Configure cache
	run: echo "cache_id=$(date --utc '+%V')" >> $GITHUB_ENV

	- name: Apply cache
	uses: actions/cache@v4
	with:
	key: mkdocs-${{ env.cache_id }}
	path: .cache
	restore-keys: \|
	mkdocs-

	- name: Install dependencies
	run: pip install -r .github/mkdocs-requirements.txt

	- name: Fetch gh-pages
	run: git fetch origin gh-pages --depth=1

	- name: Publish main branch docs
	if: github.ref_type == 'branch' && github.ref_name == 'main'
	run: mike deploy main --push

	# - name: Publish pre-release docs
	# if: github.ref_type == 'branch' && startsWith(github.ref_name, 'rel-v')
	# run: \|
	# version=`echo ${{ github.ref_name }} \| cut -d - -f 2 \| cut -d . -f 1,2`
	# mike deploy ${version} --push

	- name: Publish release docs
	if: github.ref_type == 'tag' && startsWith(github.ref_name, 'v')
	run: \|
	version=`echo ${{ github.ref_name }} \| cut -d . -f 1,2`
	mike deploy ${version} latest --update-aliases --push
	mike set-default ${version} --push --allow-empty

Provide feedback