diff options
Diffstat (limited to 'docs/en/make.bat')
| -rw-r--r-- | docs/en/make.bat | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/docs/en/make.bat b/docs/en/make.bat index 5c1494bf7..c12f0a720 100644 --- a/docs/en/make.bat +++ b/docs/en/make.bat @@ -187,4 +187,11 @@ results in %BUILDDIR%/doctest/output.txt. goto end ) +if "%1" == "pdf" ( + %SPHINXBUILD% -b pdf -t enable_rst2pdf %ALLSPHINXOPTS% %BUILDDIR%/pdf + echo. + echo.Build finished. The PDF file is in %BUILDDIR%/pdf + goto end +) + :end |