Extend GitLab CI to lint documentation
Git has several scripts to lint its documentation and to check for missing/superfluous man pages. While those are hooked up for GitHub Actions, GitLab CI does not yet have such a job. We should backfill it.
Git has several scripts to lint its documentation and to check for missing/superfluous man pages. While those are hooked up for GitHub Actions, GitLab CI does not yet have such a job. We should backfill it.