Index: doc/support/generate.sh |
diff --git a/doc/support/generate.sh b/doc/support/generate.sh |
index f5785c6447c72eefc41618e656bd0a2ef88e91fb..ad76295b351640eeffbb9f0427a3347012195ab5 100755 |
--- a/doc/support/generate.sh |
+++ b/doc/support/generate.sh |
@@ -47,6 +47,9 @@ ${sed_ext} -e 's%<a href="([^/]+)\.html">%<a href="doc/\1.html">%g' \ |
< "${output_dir}/doc/index.html" > "${output_dir}/index.html" |
rm "${output_dir}/doc/index.html" |
+# Ensure a favicon exists at the root since the browser will always request it. |
+cp doc/favicon.ico "${output_dir}/" |
+ |
# Create man/index.html |
cd "${output_dir}/man" |
cat > index.html << __EOF__ |