We have a GitHub workflow for documentation that runs make check:
|
- name: 'Check documentation' |
|
run: make -C Doc/ PYTHON=../python SPHINXOPTS="-q -W --keep-going -j4" check |
make check runs
|
check: |
|
$(SPHINXLINT) -i tools -i $(VENVDIR) -i README.rst |
|
$(SPHINXLINT) ../Misc/NEWS.d/next/ |
By default sphinx-lint only reports errors with a severity >=1:
https://github.com/sphinx-contrib/sphinx-lint/blob/b25d09c5a0cf15030c575d18078d815724a1e3e0/sphinxlint.py#L453-L459
The severity of the "default role" check (i.e. making sure that no single `...` are used), was recently changed to severity=0 in sphinx-contrib/sphinx-lint@999b43d.
This means that the use of the default role is no longer caught as an error by make check.
See also #86404.
(Thanks to @AlexWaygood for noticing the issue. cc @JulienPalard)