On Fri, 2002-08-02 at 16:30, Frédéric Crozat wrote:
>
> Another workaround is to change the font size..
As the original poster mentioned, one cannot change the font or its
size. I'd be curious if this works for anyone.
--
Steve Fox
http://k-lug.org
On Fri, 02 Aug 2002 22:36:32 +0200, Brad Felmey wrote :
> On Fri, 2002-08-02 at 19:29, gabor wrote:
>> On Fri, 2002-08-02 at 10:29, Frederic Crozat wrote:
>> > On Fri, 02 Aug 2002 16:24:50 +0200, Oliver Lemke wrote:
>> >
>> > > After the latest updates the font in the gnome-terminal changed to
>
On Fri, 2002-08-02 at 19:29, gabor wrote:
> On Fri, 2002-08-02 at 10:29, Frederic Crozat wrote:
> > On Fri, 02 Aug 2002 16:24:50 +0200, Oliver Lemke wrote:
> >
> > > After the latest updates the font in the gnome-terminal changed to bigger
> > > size and looks quite awful. On another machine ther
On Fri, 2002-08-02 at 10:29, Frederic Crozat wrote:
> On Fri, 02 Aug 2002 16:24:50 +0200, Oliver Lemke wrote:
>
> > After the latest updates the font in the gnome-terminal changed to bigger
> > size and looks quite awful. On another machine there is a layer of pipe
> > symbols scattered across th
On Fri, 02 Aug 2002 16:24:50 +0200, Oliver Lemke wrote:
> After the latest updates the font in the gnome-terminal changed to bigger
> size and looks quite awful. On another machine there is a layer of pipe
> symbols scattered across the whole terminal window. And whatever one
> selects in the pre
After the latest updates the font in the gnome-terminal changed to
bigger size and looks quite awful. On another machine there is a layer
of pipe symbols scattered across the whole terminal window. And whatever
one selects in the preferences dialog, it always uses the same font and
size. Recompila
