Le vendredi 10 octobre 2008 à 16:38 +0200, R. Bastian a écrit : > On Fri, 10 Oct 2008 13:52:54 +0200 > Victor Stinner <[EMAIL PROTECTED]> wrote: > > > Le Friday 10 October 2008 12:52:34 R. Bastian, vous avez écrit : > > > ça marche, mais les caractères de ce qui s'affiche dans le > > > terminal est trop petit; donc il faut après chaque lancement > > > augmenter la taille de l'affichage par 'Ctrl +'. > > > > 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. > > 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é ... > > > > > -- > > Victor Stinner aka haypo > > http://www.haypocalc.com/blog/ > > > Et en contournant le problème ? Mon idée, très grossièrement : au lieu d'ouvrir un Gnome-terminal, préférer un bon vieux xterm, avec l'espoir qu'il se laisse mieux configurer, vu que s'il porte bien son nom, xterm est plus directement géré par le serveur X lui-même qu'un Gnome-terminal ... ou bien ?
FD
