Re: gnome-terminal murió

[Alejandro Pinazo <alejandropinazo@eresmas.com>]

Hola:

On 03 Nov 2002 23:31:06 +0100
Rodrigo Moya <rodrigo@gnome-db.org> wrote:
 
> ¿no estás usando GNOME 2? Si no lo estás usando, entonces tendrás que
> modificar a mano ~/.gnome/Terminal. Como ya te han dicho en otro mail,
> si no puedes solucionarlo, simplemente borra el fichero, ya que se
> volverá a crear la próxima vez que uses el gnome-terminal.
> 
> saludos

Efectivamente uso GNOME 1.4.  De todas formas ya he probado lo de
modificar el archivo "$HOME/.gnome/Terminal" e incluso de borrarlo pero
"gnome-terminal" me sigue cargando con una fuente enanísima.  Éste es el
archivo de configuración que me crea:

[Placement]
Dock=Menubar\\0,0,0,0

[Config]
font=-*-fixed-medium-r-normal--14-*-*-*-*-*-*-*,*-r-*
wordclass=-A-Za-z0-9,./?%&#
scrollpos=right
bell_silenced=false
blinking=true
swap_del_and_backspace=false
del_is_del=false
meta_use_high_bit=false
meta_modifiers_mod1=true
meta_modifiers_mod2=false
meta_modifiers_mod3=false
meta_modifiers_mod4=true
meta_modifiers_mod5=false
login_by_default=false
use_bold=false --> esto lo crea a true pero yo lo cambio a false
use_im=true
use_fontset=true
scrollbacklines=100
color_set=0
color_scheme=linux
menubar=true
scrollonkey=true
scrollonoutput=false
transparent=false
shaded=false
scroll_background=false
background_pixmap=false
pixmap_file=
keyboard_secured=false
palette=rgb:0000/0000/0000 rgb:aaaa/0000/0000 rgb:0000/aaaa/0000
rgb:aaaa/5555/0000 rgb:0000/0000/aaaa rgb:aaaa/0000/aaaa
rgb:0000/aaaa/aaaa rgb:aaaa/aaaa/aaaa rgb:5555/5555/5555
rgb:ffff/5555/5555 rgb:5555/ffff/5555 rgb:ffff/ffff/5555
rgb:5555/5555/ffff rgb:ffff/5555/ffff rgb:5555/ffff/ffff
rgb:ffff/ffff/ffff rgb:bebe/bebe/bebe rgb:0000/0000/0000 

Si en font pongo cualquier otra cosa, "gnome-terminal" me da un error de
violación de segmento.  ¿Es un poco tortuoso esto de las fuentes en
Debian, no?

Un saludo.

Por cierto, Rodrigo, tus correos siempre llegan duplicados a la lista :-?