Re: [PATCH] sphinx: Use separate doctree directories for different builders

2019-10-17 Thread Peter Maydell
On Mon, 14 Oct 2019 at 16:01, Eduardo Habkost wrote: > > sphinx-build is buggy when multiple processes are using the same > doctree directory in parallel. See the 3-year-old Sphinx bug > report at: https://github.com/sphinx-doc/sphinx/issues/2946 > > Instead of avoiding parallel builds or adding

Re: [PATCH] sphinx: Use separate doctree directories for different builders

2019-10-14 Thread John Snow
On 10/14/19 11:01 AM, Eduardo Habkost wrote: > sphinx-build is buggy when multiple processes are using the same > doctree directory in parallel. See the 3-year-old Sphinx bug > report at: https://github.com/sphinx-doc/sphinx/issues/2946 > > Instead of avoiding parallel builds or adding some

[PATCH] sphinx: Use separate doctree directories for different builders

2019-10-14 Thread Eduardo Habkost
sphinx-build is buggy when multiple processes are using the same doctree directory in parallel. See the 3-year-old Sphinx bug report at: https://github.com/sphinx-doc/sphinx/issues/2946 Instead of avoiding parallel builds or adding some kind of locking, I'm using the simplest solution: just