diff --git a/doc/docinfo.html b/doc/docinfo.html
index 2fc163218..2be23cfaa 100644
--- a/doc/docinfo.html
+++ b/doc/docinfo.html
@@ -108,6 +108,10 @@ td {
   border-right: none;
 }
 
+#toc.toc2 > ul {
+  font-size: .9em;
+}
+
 @media screen and (max-width:767px) {
   #toc.toc2 {
     background-color: var(--body-bg-color);