I would like to have the ability to increase or decrease the font size beyond the 4 options now. I think that the current “Normal” size is too big and the “small” size is too small. I would prefer the ability to scale text by font size.
You can do this with custom themes using GraphQL. I have a theme that makes non-colored syntax smaller, so there must be a way. But I don’t know how to yet.