Build and Deploy #36

	name: Build and Deploy

	on:
	push:
	branches:
	- master
	workflow_dispatch:

	# This is just a guard against two of these actions
	# running at the same time. Not likely an issue for
	# us right now, but it could happen.
	concurrency: build-and-deploy-${{ github.ref }}

	jobs:
	deploy-docs:
	runs-on: ubuntu-latest

	steps:
	- name: Checkout
	uses: actions/checkout@v4

	- name: Check for changes in docs folder
	id: docs_check
	run: \|
	git fetch origin master
	if [[ $(git diff --name-only origin/${{ github.event.repository.default_branch }} -- './docs') ]]; then
	echo "There have been changes to the docs."
	echo "docs_changed=true" >> $GITHUB_OUTPUT
	else
	echo "No changes to the docs."
	echo "docs_changed=false" >> $GITHUB_OUTPUT
	fi

	- name: Deploy documentation
	if: ${{ steps.docs_check.outputs.docs_changed == 'true' }}
	uses: JamesIves/github-pages-deploy-action@v4
	with:
	folder: docs
	branch: gh-pages # default for this action, but including to be explicit

Provide feedback