PDF files already are compressed; adding gzip compression is mostly pointless.
These are not linked, though we have been generating them forever, cf. commit 4dc7b0f0df446347e8b72908b567865f2021641e Author: Daniel Berlin <[email protected]> Date: Mon Oct 17 00:48:54 2005 +0000 SVN version From-SVN: r105483 Pushed. Gerald maintainer-scripts: * update_web_docs_git: Stop generating .pdf.gz copies of .pdf files. --- maintainer-scripts/update_web_docs_git | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/maintainer-scripts/update_web_docs_git b/maintainer-scripts/update_web_docs_git index 67c6e6254ea..7bb46fb2378 100755 --- a/maintainer-scripts/update_web_docs_git +++ b/maintainer-scripts/update_web_docs_git @@ -269,7 +269,7 @@ find . -name '*.html' | while read f; do done # Then build a gzipped copy of each of the resulting .html, .ps and .tar files -for file in */*.html *.ps *.pdf *.tar; do +for file in */*.html *.ps *.tar; do cat $file | gzip --best > $file.gz done -- 2.55.0
