gitlab-ci: add job to lint docs
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.
Closes #331 (closed).
Edited by Patrick Steinhardt