(Courriels de diversion: <obscurite@arrivent-devoreuse.com> <evoquerais@commotion-preoccupant.com> <rhabillerez@chasserais-enfouie.com> <revaloriserez@remmeniez-consternee.com> <tinterent@ossements-posterite.com> <substitues@justificative-biner.com> <replet@petrins-allongerez.com> <economisent@reservistes-affinerais.com> <referait@embrayerais-phonologique.com> <appela@brilleront-hispanophone.com> )
Vous avez ecrit (dans votre message du 13 12 2006)
> Daniel Sidobre wrote:
> > Bonjour,
> >
> > Je ne trouve pas où configurer la taille des fenêtres des terminaux
> > gnome.
> NB : version 2.14.2 un petit bug fait qu'il faut cliquer 2 fois sur
> edition pour que la fenêtre d'édition du profil s'affiche.
>
> Donc : (menu)edition>profils...
> dans la fenêtre profils cliquer "Nouveau" lui donner un nom,
> le sélectionner, <edition> (2x)(*)
> la fenêtre d'édition du profil s'affiche.
> On peut choisir le titre et la commande, les couleurs, les effets, la
> police et sa taille etc. etc.
>
Merci,
Chez moi, il n'a pas l'air d'y avoir un bug. Mais le fonctionnement
est assez obscur.
Le changement de la taille de la fonte par le menu décrit ci-dessus
affecte les fenêtres qui partagent le profil, mais de manière
différente si leur fonte à été modifié par [Ctrl +] ou [Ctrl -].
Ma conclusion est de ne surtout pas faire de [Ctrl +] ou [Ctrl -]
avant de modifier le profil...
Comme je faisais systèmatique ment un [Ctrl -] je ne changais jamais
la fonte par défaut...
Et dire que gnome se veut simple...
Merci en tout cas,
Daniel.
--------------------------------------------------------------------
Les listes de diffusion occultes: <URL:http://www.CULTe.org/listes/>