pull font into editor
commit0f4aea6db747498467ab5b43a762ef3d5f39f56b
authorKartik K. Agaram <vc@akkartik.com>
Fri, 29 Dec 2023 19:18:41 +0000 (29 11:18 -0800)
committerKartik K. Agaram <vc@akkartik.com>
Fri, 29 Dec 2023 19:18:41 +0000 (29 11:18 -0800)
treeaa3f575583088865f41f0317a3470b0ec064c718
parente36559d264616cc8bc10ebbfcc429663c17fb7aa
pull font into editor

Now it adjusts the current font for itself.
And it's up to the caller to adjust the current font after.
edit.lua
log_browser.lua
run.lua
source.lua
source_edit.lua