diff --git a/doc/gnu_docs/index.html b/doc/gnu_docs/index.html index 985c1e9801..fb7e80eb95 100644 --- a/doc/gnu_docs/index.html +++ b/doc/gnu_docs/index.html @@ -27,7 +27,7 @@