diff options
| author | Julien Palard <julien@palard.fr> | 2022-02-10 07:59:04 (GMT) |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-02-10 07:59:04 (GMT) |
| commit | b878b3af0b3a9e3ab3ffcaf90a4066dfb3bb7cac (patch) | |
| tree | ecf60e1ac5b98d751865622cc48364cf582b7d9c /Doc/make.bat | |
| parent | b71dc71905ab674ccaa4a56230d17a28f61c325c (diff) | |
| download | cpython-b878b3af0b3a9e3ab3ffcaf90a4066dfb3bb7cac.zip cpython-b878b3af0b3a9e3ab3ffcaf90a4066dfb3bb7cac.tar.gz cpython-b878b3af0b3a9e3ab3ffcaf90a4066dfb3bb7cac.tar.bz2 | |
bpo-42238: [doc] moving from rstlint.py to sphinx-lint. (GH-31097)
Diffstat (limited to 'Doc/make.bat')
| -rw-r--r-- | Doc/make.bat | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/Doc/make.bat b/Doc/make.bat index 7fde063..9eaaa46 100644 --- a/Doc/make.bat +++ b/Doc/make.bat @@ -36,6 +36,16 @@ if not defined BLURB ( set BLURB=%PYTHON% -m blurb ) +if not defined SPHINXLINT ( + %PYTHON% -c "import sphinxlint" > nul 2> nul + if errorlevel 1 ( + echo Installing sphinx-lint with %PYTHON% + %PYTHON% -m pip install sphinx-lint + if errorlevel 1 exit /B + ) + set SPHINXLINT=%PYTHON% -m sphinxlint +) + if "%1" NEQ "htmlhelp" goto :skiphhcsearch if exist "%HTMLHELP%" goto :skiphhcsearch @@ -168,7 +178,7 @@ if EXIST "%BUILDDIR%\html\index.html" ( goto end :check -cmd /S /C "%PYTHON% tools\rstlint.py -i tools" +cmd /S /C "%SPHINXLINT% -i tools" goto end :serve |