v0.19.0 #128

	---
	name: Release Documentation

	on:
	release:
	types:
	- published

	jobs:
	build:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: "true"
	lfs: true
	- uses: julia-actions/setup-julia@latest
	with:
	version: 1.9.4
	- name: Install dependencies
	run: julia --color=yes --project=docs/ -e 'using Pkg; Pkg.develop(PackageSpec(path=pwd()))'
	- name: Build and deploy
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	run: \|
	export RELEASE_VERSION=$(echo $GITHUB_REF \| awk -F / '{print $3}')
	# we release via the Github UI, which also creates a tag but does not push to the repo. documenter wants
	# to see a tag push event though, which we now provide artificially:
	export GITHUB_EVENT_NAME=push
	julia --color=yes --project=docs/ -e 'using Pkg; Pkg.develop(PackageSpec(path=pwd())); Pkg.resolve(); include("docs/make.jl")'

Provide feedback