Gnome terminal patch

["Gustavo M. Giráldez" <gustavo dynaweb com ar>]

Hi!

I was redirected here by George, which I thought was the gnome-terminal
mantainer (thanks George). This patch allows you to choose the terminal
font from a user-definable list from the popup menu. The font list is
saved in the config file, and the configuration format is backward
compatible. Also I found (using memprof) and fixed some minor memory
leaks.

This is my first contribution to Gnome and hope it's not the last. I
learned lots by making this patch, and it was fun. I hope you find it
useful.

Cheers,


Gustavo Giráldez

gnome-terminal.patch.gz