> Victor Stinner <[EMAIL PROTECTED]> wrote: >> Tu ne peux pas changer la configuration du terminal Gnome (taille de la >> police) pour changer la taille de la police par défaut ? Regarde les menus du >> terminal.
2008/10/10 R. Bastian <[EMAIL PROTECTED]>: > J'ai regardé et, comme dit, je peux changer la barre (ou > de cadre) "Fichier Edition Affichage Terminal Onglets Aide". > Dans "Affichage", on propose, comme dit, <Ctrl +>, > mais à la fin de la session, tout est oublié ... Menu Système > Préférences > Apparence, onglet Polices, "Police à chasse fixe" devrait te permettre de changer la police utilisée dans le terminal. -- Alexandre Franke
