diff options
author | Ihor Nehrutsa <Ihor.Nehrutsa@gmail.com> | 2021-09-10 08:44:03 +0300 |
---|---|---|
committer | Damien George <damien@micropython.org> | 2021-09-13 18:15:38 +1000 |
commit | c7842f479836e4aec449a83ddf2907d28dde6027 (patch) | |
tree | 2bef41c05997e115bcf446135e78e9a05782c7ac /docs/make.bat | |
parent | 0a510737248132430de4317d7fd4d47e76862182 (diff) |
docs/make.bat: Change Windows output dir from '_build' to 'build'.
To match the output file used by Makefile.
Diffstat (limited to 'docs/make.bat')
-rw-r--r-- | docs/make.bat | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/make.bat b/docs/make.bat index c09487fb7..2a9e670e4 100644 --- a/docs/make.bat +++ b/docs/make.bat @@ -5,7 +5,7 @@ REM Command file for Sphinx documentation if "%SPHINXBUILD%" == "" ( set SPHINXBUILD=sphinx-build ) -set BUILDDIR=_build +set BUILDDIR=build set SPHINXOPTS=-W --keep-going set ALLSPHINXOPTS=-d %BUILDDIR%/doctrees %SPHINXOPTS% . set I18NSPHINXOPTS=%SPHINXOPTS% . |