From: Andre Noll <maan@tuebingen.mpg.de>
Date: Fri, 10 May 2024 23:27:09 +0000 (+0200)
Subject: index.html: Adjust font size for code.
X-Git-Tag: v1.0.2~10
X-Git-Url: http://git.tue.mpg.de/?a=commitdiff_plain;h=ac9ab4fd32bd337b5ea7a5219ae485886faa9806;p=dss.git

index.html: Adjust font size for code.

At least on some firefox versions, the characters of the default
monospace font look a bit small.
---

diff --git a/index.html.m4 b/index.html.m4
index 23b3933..a4b3dd6 100644
--- a/index.html.m4
+++ b/index.html.m4
@@ -15,6 +15,9 @@ dnl SPDX-License-Identifier: GPL-2.0
 		a {
 			color: #4444ff;
 		}
+		pre,code {
+			font-size: 110%;
+		}
 	</style>
 	<link rel="shortcut icon" href="dss.ico">
 </head>