- ouverture d'un gnome-terminal - clic droit dans la fenetre - editer le profil courant- je dois decocher l'option "utiliser la meme taille de police que les autres applications"
- et la je choisie comme je veux... ok ca marche... merci de votre aide.... David