r8573: set file properties

diff --git a/doc/html.tar.gz b/doc/html.tar.gz
index a614e8bf10aa30bec14ea8ed62e7ec7b43372c25..3bf876cde6c69dd27572e45f8dc003583a448a2b 100644 (file)
Binary files a/doc/html.tar.gz and b/doc/html.tar.gz differ