| 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__
|
|
|