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. Recompilation didn't help.
Any ideas??? -- Oliver Lemke University of Bremen - Institute of Environmental Physics Satellite Microwave Atmospheric Sounding Group
