From 6721502d324d3d0475c27455bcbe247c741093a7 Mon Sep 17 00:00:00 2001 From: Koen Lagveen Date: Mon, 3 Jul 2023 21:06:55 +0200 Subject: [PATCH] change default font and theme --- index.js | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/index.js b/index.js index 8fb9d7b..0728437 100644 --- a/index.js +++ b/index.js @@ -24,10 +24,10 @@ const filters = { } const selectTheme = () => { - let theme = 'monokai' + let theme = 'oceanic-next' if (input.selectedIndex > -1) { - theme = input.options[input.selectedIndex].innerHTML + theme = input.options[input.selectedIndex].textContent } editor.setOption('theme', theme) document.cookie = `theme=${theme};max-age=172800` @@ -40,7 +40,7 @@ const selectFont = () => { const codeMirror = document.querySelector('.CodeMirror') if (!font) { - font = 'cartograph' + font = 'source-code-pro' msg.innerHTML = 'Test drive all the programming fonts!' } else if (typeof fontData !== 'undefined') { msg.innerHTML = `Test drive ${fontData[font].name}!`