Merge branch 'jt/port-ci-whitespace-check-to-gitlab'

The "whitespace check" task that was enabled for GitHub Actions CI
has been ported to GitLab CI.

* jt/port-ci-whitespace-check-to-gitlab:
  gitlab-ci: add whitespace error check
  ci: make the whitespace report optional
  ci: separate whitespace check script
  github-ci: fix link to whitespace error
  ci: pre-collapse GitLab CI sections

diff --cc .gitlab-ci.yml
Simple merge

diff --cc ci/lib.sh
Simple merge