2023-11-15 14:06:56 +00:00
|
|
|
on.keychord_press = function(chord, key)
|
2023-11-15 17:27:34 +00:00
|
|
|
if chord == 'C-=' then
|
|
|
|
update_font_settings(Editor_state.font_height+2)
|
|
|
|
elseif chord == 'C--' then
|
|
|
|
update_font_settings(Editor_state.font_height-2)
|
|
|
|
elseif chord == 'C-0' then
|
|
|
|
update_font_settings(20)
|
|
|
|
else
|
|
|
|
edit.keychord_press(Editor_state, chord, key)
|
|
|
|
end
|
2023-11-15 14:06:56 +00:00
|
|
|
end
|