check-cmdref.sh
#!/usr/bin/env bash
set -o errexit
set -o nounset
set -o pipefail
script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
cmdref_dir="${script_dir}/cmdref"
if ! git diff --quiet -- "${cmdref_dir}" ; then
git --no-pager diff "${cmdref_dir}"
echo "HINT: to fix this, run 'make -C Documentation update-cmdref'"
exit 1
fi