home: terminal: remove DPI workaround

And instead change the font size to be *about* right.
This commit is contained in:
Bruno BELANYI 2023-02-12 17:12:19 +00:00
parent f89e10fdca
commit 4f883b0198

View file

@ -8,13 +8,8 @@ in
enable = true; enable = true;
settings = { settings = {
env = {
# DPI scaling means the font is way too big otherwise
WINIT_X11_SCALE_FACTOR = "1.0";
};
font = { font = {
size = 9; size = 5.5;
}; };
colors = { colors = {