diff options
| -rwxr-xr-x | scripts/docs-build.sh | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/scripts/docs-build.sh b/scripts/docs-build.sh index 2e2b79b04..466219f83 100755 --- a/scripts/docs-build.sh +++ b/scripts/docs-build.sh @@ -208,12 +208,10 @@ do mkdir -p "$output" - sphinx-build -b html -t html -E "$src" "$output" - { - sphinx-build -b singlehtml -t singlehtml -E "$src" "${output}-single" + sphinx-build -b singlehtml -t singlehtml -E "$src" "$output" } || { - msg="Error: Single HTML creation for $dir has failed." + msg="Error: HTML creation for $dir has failed." echo echo "$msg" echo |