TRIVIAL: Update release instructions #16

	name: missing-commits

	on:
	# TODO: Remove the next line before merging
	pull_request:
	push:
	branches:
	# Only check that the branches are up to date when updating the
	# relevant branches.
	# TODO: Uncomment the next lines before merging
	# - develop
	# - release

	jobs:
	check:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v4
	with:
	fetch-depth: 0
	- name: Check for missing commits
	id: commits
	env:
	SUGGESTION: \|

	If you are reading this, then there are commits that are
	missing from "develop" and/or "release". Do a reverse-merge
	as soon as possible. See CONTRIBUTING.md for instructions.
	run: \|
	set -o pipefail
	# Branches ordered by how "canonical" they are. Every commit in
	# one branch should be in all the branches behind it
	order=( master release develop )
	branches=()
	for branch in "${order[@]}"
	do
	# Check that the branches exist so that this job will work on
	# forked repos, which don't necessarily have master and
	# release branches.
	if git ls-remote --exit-code --heads origin \
	refs/heads/${branch} > /dev/null
	then
	branches+=( origin/${branch} )
	fi
	done

	prior=()
	for branch in "${branches[@]}"
	do
	if [[ ${#prior[@]} -ne 0 ]]
	then
	echo "Checking ${prior[@]} for commits missing from ${branch}"
	git log --oneline --no-merges "${prior[@]}" \
	^$branch \| tee -a "missing-commits.txt"
	fi
	prior+=( "${branch}" )
	done
	if [[ $( cat missing-commits.txt \| wc -l ) -ne 0 ]]
	then
	echo "${SUGGESTION}"
	exit 1
	fi

Provide feedback