Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
doc build: work-around for #11727 can be removed
This issue has been fixed. We can now show docbuild output even if the build fails.
- Loading branch information