diff --git a/doc/contents.html b/doc/contents.html index 5f35b8fdc..5f3a05097 100644 --- a/doc/contents.html +++ b/doc/contents.html @@ -6,7 +6,7 @@