This change will make things strictly better for new users (without an existing
configuration file) and has no effect on existing users.
The tools should be fairly uncontentious, I hope, especially as they only serve
as a starting point anyway: users can quickly delete what they don’t want, or
change it into what they prefer.
But having something is strictly better than having nothing :)
We make some space in the config file by removing the old paragraph about pixel
fonts, which seems rather outdated and irrelevant to me.
72975d6764