GHA: complain if PR adds commits from people not yet listed in ./AUTHORS

not to have to update ./AUTHORS or .mailmap after merging.

.github/workflows/authors-file.bash

@@ -0,0 +1,25 @@
+#!/bin/bash
+set -exo pipefail
+
+sort -uo AUTHORS AUTHORS
+git add AUTHORS
+
+git log --format='format:%aN <%aE>' "$(
+  git merge-base "$GITHUB_BASE_REF" "$GITHUB_HEAD_REF"
+)..$GITHUB_HEAD_REF" >> AUTHORS
+
+sort -uo AUTHORS AUTHORS
+git diff AUTHORS >> AUTHORS.diff
+
+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
+  false
+fi

.github/workflows/authors-file.yml

@@ -0,0 +1,16 @@
+name: AUTHORS file
+
+on:
+  pull_request: { }
+
+jobs:
+  authors-file:
+    name: AUTHORS file
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout HEAD
+        uses: actions/checkout@v3
+
+      - name: Check whether ./AUTHORS is up-to-date
+        run: ./authors-file.bash

CONTRIBUTING.md

@@ -111,6 +111,12 @@ refs #1234
 You can add multiple commits during your journey to finish your patch.
 Don't worry, you can squash those changes into a single commit later on.
 
+Ensure your name and email address in the commit metadata are correct.
+In your first contribution (PR) also add them to [AUTHORS](./AUTHORS).
+If those metadata changed since your last successful contribution,
+you should update [AUTHORS](./AUTHORS) and [.mailmap](./.mailmap).
+For the latter see [gitmailmap(5)](https://git-scm.com/docs/gitmailmap).
+
 ## <a id="contributing-pull-requests"></a> Pull Requests
 
 Once you've commited your changes, please update your local master