From d24ea631207ac02e1f17dd4c5026192c4064dfb3 Mon Sep 17 00:00:00 2001
From: qqii <QiruiChen97@gmail.com>
Date: Sun, 8 Jan 2023 02:37:22 +0000
Subject: [PATCH] Fix #126 line number spacing not updating on zoom

This also fixes the cursor and selected line spacing not updating, which
is most obvious whet adjusting the line spacing.
Manually firing a refresh event for selectLanguage is not necessary as
it calls editor.setOption which fires this event internally.
---
 index.js | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/index.js b/index.js
index edb0940..abf0e3d 100644
--- a/index.js
+++ b/index.js
@@ -81,12 +81,14 @@ function setSize() {
 
     document.querySelector('.CodeMirror').style.fontSize = `${size}px`;
     document.cookie = `size=${size};max-age=172800`;
+    editor.refresh();
 }
 function setSpacing() {
     var spacing = document.getElementById('spacing').value;
 
     document.querySelector('.CodeMirror').style.lineHeight = spacing;
     document.cookie = `spacing=${spacing};max-age=172800`;
+    editor.refresh();
 }
 function selectLanguage() {
     var lang = document.getElementById('select-language').value;