[PATCH 0/4] Documentation: improve linting of manpage existence

Hi,

in [1], Junio noticed that `make check-docs` was failing for a recent patch series of mine that introduces the new git-refs(1) command. Curiously though, while the checks do print errors, the Makefile target itself succeeded and thus did not make the corresponding CI job fail.

This patch series fixes that issue and also refactors the infrastructure such that it fits better into our existing set of linter targets for our documentation. Finally, this series then adds a job to GitLab CI that is equivalent to the job we already have on GitHub Actions.

[1]: <xmqqjzj9czop.fsf@gitster.g>

Patrick

Patrick Steinhardt (4):
  Makefile: extract script to lint missing/extraneous manpages
  Documentation/lint-manpages: bubble up errors
  gitlab-ci: add job to run `make check-docs`
  ci/test-documentation: work around SyntaxWarning in Python 3.12

 .gitlab-ci.yml                 |   9 +++
 Documentation/Makefile         |   4 ++
 Documentation/lint-manpages.sh | 107 +++++++++++++++++++++++++++++++++
 Makefile                       |  36 -----------
 ci/test-documentation.sh       |   1 +
 5 files changed, 121 insertions(+), 36 deletions(-)
 create mode 100755 Documentation/lint-manpages.sh