Merge pull request #863 from jgmdev/scale-fix
plugin scale: replace non existing font.set_size with font.copy
This commit is contained in:
commit
d82b668a09
|
@ -50,12 +50,8 @@ local function set_scale(scale)
|
||||||
style.code_font = renderer.font.copy(style.code_font, s * style.code_font:get_size())
|
style.code_font = renderer.font.copy(style.code_font, s * style.code_font:get_size())
|
||||||
end
|
end
|
||||||
|
|
||||||
for _, font in pairs(style.syntax_fonts) do
|
for name, font in pairs(style.syntax_fonts) do
|
||||||
renderer.font.set_size(font, s * font:get_size())
|
style.syntax_fonts[name] = renderer.font.copy(font, s * font:get_size())
|
||||||
end
|
|
||||||
|
|
||||||
for _, font in pairs(style.syntax_fonts) do
|
|
||||||
renderer.font.set_size(font, s * font:get_size())
|
|
||||||
end
|
end
|
||||||
|
|
||||||
-- restore scroll positions
|
-- restore scroll positions
|
||||||
|
|
Loading…
Reference in New Issue