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.yml

@@ -0,0 +1,39 @@
+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