Deploy Docs #4

	name: Deploy Docs

	on:
	push:
	tags:
	- "*"
	workflow_dispatch:
	inputs:
	version:
	description: "Documentation version to deploy, e.g. 0.1.0"
	required: true
	type: string

	permissions:
	contents: write

	jobs:
	deploy:
	runs-on: ubuntu-latest

	steps:
	- name: Check out repository
	uses: actions/checkout@v4
	with:
	fetch-depth: 0

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

	- name: Install documentation dependencies
	run: pip install -r requirements-dev.txt

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

	- name: Resolve version
	id: version
	shell: bash
	run: \|
	if [ "${{ github.event_name }}" = "workflow_dispatch" ]; then
	VERSION="${{ github.event.inputs.version }}"
	else
	VERSION="${GITHUB_REF_NAME}"
	fi
	echo "version=$VERSION" >> "$GITHUB_OUTPUT"

	- name: Deploy versioned docs with mike
	run: \|
	mike deploy --push --update-aliases "${{ steps.version.outputs.version }}" latest
	mike set-default --push latest

Provide feedback