diff options
| -rwxr-xr-x | configure | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/configure b/configure index 9b1f5b33e4..25f7d91572 100755 --- a/configure +++ b/configure @@ -4942,7 +4942,9 @@ has_sphinx_build() { # sphinx-build doesn't exist at all or if it is too old. mkdir -p "$TMPDIR1/sphinx" touch "$TMPDIR1/sphinx/index.rst" - "$sphinx_build" $sphinx_werror -c "$source_path/docs" -b html "$TMPDIR1/sphinx" "$TMPDIR1/sphinx/out" >/dev/null 2>&1 + "$sphinx_build" $sphinx_werror -c "$source_path/docs" \ + -b html "$TMPDIR1/sphinx" \ + "$TMPDIR1/sphinx/out" >> config.log 2>&1 } # Check if tools are available to build documentation. |