diff --git a/doc/index.html b/doc/index.html index c6e0722e..5ec32a6b 100644 --- a/doc/index.html +++ b/doc/index.html @@ -134,6 +134,8 @@ among others.