diff options
| -rwxr-xr-x | scripts/docs-build.sh | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/scripts/docs-build.sh b/scripts/docs-build.sh index 043fd1b94..74144ff55 100755 --- a/scripts/docs-build.sh +++ b/scripts/docs-build.sh @@ -220,6 +220,18 @@ do sphinx-build -b html -t html -E "$src" "$output" + { + sphinx-build -b singlehtml -t singlehtml -E "$src" "${output}-single" + } || { + msg="Error: Single HTML creation for $dir has failed." + echo + echo "$msg" + echo + if [ -n "$GERRIT_COMMENT" ]; then + echo "$msg" >> "$GERRIT_COMMENT" + fi + } + # Note: PDF creation may fail in project doc builds. # We allow this build job to be marked as succeeded with # failure in PDF creation, but leave message to fix it. |