diff --git a/doc/index.html b/doc/index.html index 9ddd65d3..4550be5c 100644 --- a/doc/index.html +++ b/doc/index.html @@ -116,7 +116,7 @@ among others.