From 8310cf053046d33830a6d16eb285837da8702774 Mon Sep 17 00:00:00 2001
From: Michael Mueller <michael.mueller@uos.de>
Date: Tue, 21 Jan 2025 15:12:32 +0100
Subject: [PATCH] Increased font size in VSCode.

---
 .vscode/settings.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.vscode/settings.json b/.vscode/settings.json
index 04155ba200..a4f0c0c941 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -158,7 +158,7 @@
     "html.format.wrapLineLength": 80,
     "editor.wordWrap": "bounded",
     "editor.wordWrapColumn": 90,
-    "editor.fontSize": 12,
+    "editor.fontSize": 13,
     "terminal.integrated.shellIntegration.suggestEnabled": true,
     "git.mergeEditor": true,
     "merge-conflict.autoNavigateNextConflict.enabled": true,