Modification de la police de l'éditeur de texte par défaut
Vous pouvez modifier la police de l'éditeur de texte par défaut dans la page des préférences
de Editeur de texte par défaut (Fenêtre > Préférences > Plan de travail > Editeur
de texte par défaut).