Bonjour tout le monde,


Ma question est simple: comment faire pour changer la police par défaut de cet éditeur?


Je ne vois pas de ligne y faisant référence dans le fichier de configuration.


Merci beaucoup!