Dmitry Gutov<dmitry@gutov.dev> writes:
I'll have to revisit the branch, but an icon set that is off by
default is about just as useful for improving the default look of the
editor as the ability to toggle the tool-bar off. Which is to say,
very little improvement over the status quo.
Useful or not, it's what we decided, and there are yet no reasons to
reconsider this decision.
I'm sorry about downplaying the amount of effort that went into this,
though. Let me take a second look at the proposed set this
evening. Too bad we don't have a page with an overview - or it's lost
in some older thread.
If it helps, most of the discussion took place in August 2022.