From 37218e876484362b997e85264050293e4be35dec Mon Sep 17 00:00:00 2001
From: Felix Roos <roos@entrecode.de>
Date: Mon, 25 Apr 2022 22:04:51 +0200
Subject: [PATCH] match font size of old editor

---
 repl/src/themes/material-palenight.js | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/repl/src/themes/material-palenight.js b/repl/src/themes/material-palenight.js
index 0f219155..5ee559c9 100644
--- a/repl/src/themes/material-palenight.js
+++ b/repl/src/themes/material-palenight.js
@@ -26,13 +26,14 @@ export const materialPalenightTheme = EditorView.theme(
     '&': {
       color: '#ffffff',
       backgroundColor: background,
-      fontSize: '16px',
+      fontSize: '15px',
       'z-index': 11,
     },
 
     // done
     '.cm-content': {
       caretColor: cursor,
+      lineHeight: '22px',
     },
     '.cm-line': {
       background: '#2C323699',