diff options
| -rw-r--r-- | docs/make.bat | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/docs/make.bat b/docs/make.bat index 65602aa160..4743692ca3 100644 --- a/docs/make.bat +++ b/docs/make.bat @@ -34,6 +34,7 @@ if "%1" == "help" ( echo. changes to make an overview over all changed/added/deprecated items echo. linkcheck to check all external links for integrity echo. doctest to run all doctests embedded in the documentation if enabled + echo. spelling to check for typos in documentation goto end ) @@ -186,4 +187,13 @@ results in %BUILDDIR%/doctest/output.txt. goto end ) +if "%1" == "spelling" ( + %SPHINXBUILD% -b spelling %ALLSPHINXOPTS% %BUILDDIR%/spelling + if errorlevel 1 exit /b 1 + echo. + echo.Check finished. Wrong words can be found in %BUILDDIR%/^ +spelling/output.txt. + goto end +) + :end |