From f734fb5aac06dea594e1012945439e1985b550cc Mon Sep 17 00:00:00 2001
From: Andre Noll <maan@tuebingen.mpg.de>
Date: Sat, 11 May 2024 01:27:09 +0200
Subject: [PATCH] index.html: Adjust font size for code.

At least on some firefox versions, the characters of the default
monospace font look a bit small.
---
 index.html.m4 | 3 +++
 1 file changed, 3 insertions(+)

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>
-- 
2.39.2