From ae891ab3229d81558615555bf0dc1eb8f90b3ac8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Helleu?= <flashcode@flashtux.org>
Date: Sat, 4 Dec 2021 15:38:47 +0100
Subject: [PATCH] doc: reduce font size in table of contents

---
 doc/docinfo.html | 4 ++++
 1 file changed, 4 insertions(+)

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