pages

chore: add search functionality to docs site (#12) #10

	name: pages

	on:
	pull_request:
	branches: [main]
	push:
	tags:
	- '*'

	jobs:
	lint:
	runs-on: ubuntu-latest
	if: github.event_name == 'pull_request'
	steps:
	- uses: actions/checkout@v4
	- name: install requirements
	run: \|
	sudo apt update
	sudo apt install nodejs npm
	sudo npm install -g markdownlint-cli
	- name: lint
	run: \|
	shopt -s globstar
	shopt -s extglob
	make docs-lint

	test:
	runs-on: ubuntu-latest
	if: github.event_name == 'pull_request'
	steps:
	- uses: actions/checkout@v4
	- name: set up Python 3.11
	uses: actions/setup-python@v5
	with:
	python-version: 3.11
	- name: install dependencies
	run: \|
	python -m pip install --upgrade pip
	pip install -e .[dev]
	- name: test the site builds
	run: make docs-build

	deploy:
	runs-on: ubuntu-latest
	if: startsWith(github.ref, 'refs/tags/')
	steps:
	- uses: actions/checkout@v4
	- name: set up Python 3.11
	uses: actions/setup-python@v5
	with:
	python-version: 3.11
	- name: install dependencies
	run: \|
	python -m pip install --upgrade pip
	pip install -e .[dev]
	- name: get tag
	id: tag
	run: \|
	ref="${GITHUB_REF}"
	tag=$(echo $GITHUB_REF \| sed 's/refs\/tags\///g')
	echo "tag=$tag" >> $GITHUB_OUTPUT
	- name: deploy
	# the below steps are referenced from
	# https://github.com/jimporter/mike#deploying-via-ci
	run: \|
	git fetch origin gh-pages --depth=1
	git config user.name github-actions
	git config user.email [email protected]
	mike deploy --push --update-aliases ${{ steps.tag.outputs.tag }} latest
	mike set-default --push latest

Provide feedback