doc: reduce font size in table of contents

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);