diff options
| author | Ezio Melotti <ezio.melotti@gmail.com> | 2022-05-15 15:34:52 (GMT) |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-05-15 15:34:52 (GMT) |
| commit | 953ab0795243900ccccaaca069d932730a86fc20 (patch) | |
| tree | c3b8bfeca4033197cd5a264f9211b3c1413daaf7 /Doc/make.bat | |
| parent | 26a162baef96d78656e189b2fa16fdcab7195730 (diff) | |
| download | cpython-953ab0795243900ccccaaca069d932730a86fc20.zip cpython-953ab0795243900ccccaaca069d932730a86fc20.tar.gz cpython-953ab0795243900ccccaaca069d932730a86fc20.tar.bz2 | |
Restore default role check in `make check`. (#92290)
* Restore default role check in `make check`.
* Options first, then files.
* Update `make.bat` too.
* Add a comment explaining the extra options.
* No reason to ignore the README.rst.
* Enable default-role check in sphinx-lint.
Co-authored-by: Julien Palard <julien@palard.fr>
* Update sphinx-lint default-role check.
* Fix use of the default role in the docs.
* Update make.bat to check for the default role too.
* Fix comment in make.bat.
Co-authored-by: Julien Palard <julien@palard.fr>
Diffstat (limited to 'Doc/make.bat')
| -rw-r--r-- | Doc/make.bat | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Doc/make.bat b/Doc/make.bat index d9a7aa4..4f0b3c1 100644 --- a/Doc/make.bat +++ b/Doc/make.bat @@ -180,7 +180,10 @@ if EXIST "%BUILDDIR%\html\index.html" ( goto end :check -cmd /S /C "%SPHINXLINT% -i tools" +rem Check the docs and NEWS files with sphinx-lint. +rem Ignore the tools dir and check that the default role is not used. +cmd /S /C "%SPHINXLINT% -i tools --enable default-role" +cmd /S /C "%SPHINXLINT% --enable default-role ..\Misc\NEWS.d\next\ " goto end :serve |