sphinx: Use separate doctree directories for different builders
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 using a different
doctree cache for each builder.
Reviewed-by: Peter Maydell <[email protected]>
Signed-off-by: Eduardo Habkost <[email protected]>
Reviewed-by: John Snow <[email protected]>
Message-id:
20191014150133[email protected]
Signed-off-by: Peter Maydell <[email protected]>