diff --git a/doc/index.html b/doc/index.html index 0519588b0d..5eb84e2ea7 100644 --- a/doc/index.html +++ b/doc/index.html @@ -10,6 +10,10 @@