@pinailleur
Heldwin wrote:Bah en installant gnome-terminal, je vois bien une option dans "Préférences".
Sous le profil "Sans nom": Police personnalisée
Si tu indiquais le nom du terminal exact, ça pourrait aider...
D'après ce que j'ai compris de ton dernier message, tu es sous Gnome ?
Donc, si c'est le cas, je ne comprends pas ton problème, car il y a bien la possibilité de changer la police dans gnome-terminal.