custom editor size #345

2026-04-19 21:16:00 +00:00 · 2022-08-19 15:10:04 +02:00
parent f80c6fec99
commit 7c87baf451
3 changed files with 19 additions and 5 deletions
--- a/packages/web/src/query/AceEditor.svelte
+++ b/packages/web/src/query/AceEditor.svelte
@@ -49,6 +49,7 @@
    { label: '15', value: '15' },
    { label: '16', value: '16' },
    { label: '17', value: '17' },
+    { label: 'Custom', value: 'custom' },
  ];
 </script>

@@ -433,7 +434,7 @@
    });
    defaultFontSize = editor.getFontSize();
    if ($currentEditorFontSize) {
-      editor.setFontSize($currentEditorFontSize);
+      editor.setFontSize(parseInt($currentEditorFontSize) || 12);
    }

    editor.on('changeSelection', () => {