v0.15.0 #35

	name: Documentation

	on:
	release:
	types: [published]

	jobs:
	publish:
	if: ${{ !github.event.release.prerelease }}
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	- name: Setup Python
	uses: actions/setup-python@v5
	with:
	python-version: '3.12'
	- name: Setup Node.js
	uses: actions/setup-node@v4
	with:
	node-version: '22'
	- name: Install dependencies
	run: npm ci
	- name: Prepare
	run: python prepare/main.py
	- name: Build
	run: npm run build
	- name: Build documentation
	run: npm run doc:html
	- name: Publish
	run: \|
	# Create a temporary directory
	export temp_dir=`mktemp -d -p ~`

	(
	# Preserve .git
	mv .git $temp_dir
	cd $temp_dir

	# Switch branch
	git fetch
	git checkout gh-pages
	)

	(
	# Go to docs directory
	cd docs

	# Set no Jekyll
	touch .nojekyll

	# Move .git
	mv $temp_dir/.git .

	# Set commit identity
	git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
	git config user.name "github-actions[bot]"

	# Publish
	git add .
	if [ -n "$(git status --porcelain)" ]; then
	git commit -m "Publish `TZ='Asia/Hong_Kong' date`"
	git push -f origin gh-pages
	fi
	)

Provide feedback