Manual merge of into .

2021-11-23 15:57:22 -05:00
parent 955acf53a3 43a6e21135
commit 96db380c73
44 changed files with 2789 additions and 311 deletions
@@ -54,6 +54,10 @@ local function set_scale(scale)
    renderer.font.set_size(font, s * font:get_size())
  end

+  for _, font in pairs(style.syntax_fonts) do
+    renderer.font.set_size(font, s * font:get_size())
+  end
+
  -- restore scroll positions
  for view, n in pairs(scrolls) do
    view.scroll.y = n * (view:get_scrollable_size() - view.size.y)