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. -- Victor Stinner aka haypo http://www.haypocalc.com/blog/
