Files
backup/src/plugins/core
Mike Sawka 61de455b90 terminal font-size updates (margins, paddings, etc.) (#315)
* reorganize line styles, split lines.less into lines.less and line.less

* switch everyone to use termFontSize getter (easier to find usages)

* better font-family font-size update logic

* update line styles, clean up more

* replace icons, fix line heights

* make paddings/margins more consistent

* fix more margins, make command completions use termfontfamily

* updates for cmdinput margins, font sizes, etc.

* fix more font sizes and margins (mostly command input)

* add comment
2024-02-23 09:39:27 -08:00
..