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

Message

Patrick Steinhardt June 5, 2024, 5:16 a.m. UTC

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