diff --git a/doc/index.html b/doc/index.html index 95c3aeeb775..f687c1495c3 100644 --- a/doc/index.html +++ b/doc/index.html @@ -86,6 +86,8 @@