match font size of old editor

2026-01-11 21:58:37 +00:00 · 2022-04-25 22:04:51 +02:00 · 2022-04-25 22:04:51 +02:00 · 37218e8764
commit 37218e8764
parent 069fff673a
1 changed files with 2 additions and 1 deletions
--- 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',