CHANGELOG.md: add v2.13.10 #674

	name: AUTHORS file

	on:
	pull_request: { }

	jobs:
	authors-file:
	name: AUTHORS file
	runs-on: ubuntu-latest

	steps:
	- name: Checkout HEAD
	uses: actions/checkout@v3
	with:
	fetch-depth: 0

	- name: Check whether ./AUTHORS is up-to-date
	run: \|
	set -exo pipefail
	sort -uo AUTHORS AUTHORS
	git add AUTHORS
	git log --format='format:%aN <%aE>' "$(
	git merge-base HEAD^1 HEAD^2
	)..HEAD^2" >> AUTHORS
	sort -uo AUTHORS AUTHORS
	git diff AUTHORS >> AUTHORS.diff

	- name: Complain if ./AUTHORS isn't up-to-date
	run: \|
	if [ -s AUTHORS.diff ]; then
	cat <<'EOF' >&2
	There are the following new authors. If the commit author data is correct,
	either add them to the AUTHORS file or update .mailmap. See gitmailmap(5) or:
	https://git-scm.com/docs/gitmailmap
	Don't hesitate to ask us for help if necessary.
	EOF
	cat AUTHORS.diff
	exit 1
	fi

Provide feedback