diff options
Diffstat (limited to 'docs/make.bat')
| -rw-r--r-- | docs/make.bat | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/docs/make.bat b/docs/make.bat index d6299521eb..d7f54b2059 100644 --- a/docs/make.bat +++ b/docs/make.bat @@ -29,6 +29,7 @@ if "%1" == "help" ( echo. latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter echo. text to make text files echo. man to make manual pages + echo. texinfo to make a Texinfo source file echo. gettext to make PO message catalogs echo. changes to make an overview over all changed/added/deprecated items echo. linkcheck to check all external links for integrity @@ -143,6 +144,14 @@ if "%1" == "man" ( goto end ) +if "%1" == "texinfo" ( + %SPHINXBUILD% -b texinfo %ALLSPHINXOPTS% %BUILDDIR%/texinfo + if errorlevel 1 exit /b 1 + echo. + echo.Build finished. The Texinfo files are in %BUILDDIR%/texinfo. + goto end +) + if "%%1" == "gettext" ( %SPHINXBUILD% -b gettext %I18NSPHINXOPTS% %BUILDDIR%/locale if errorlevel 1 exit /b 1 |