Re: gnome-terminal patch

[Miguel de Icaza <miguel gnu org>]

> I added a new feature to the gnome-terminal. The included patch adds a new
> item ("Set title ...") to the menubar and the popup menu. It opens a
> dialog where you can enter a new title for the gnome-terminal window. I
> think its quite useful if you have a lot of terminal windows open and try
> to distinguish them.

I am not sure if I like this patch, there are many reasons:

  1. Setting the title of the terminal can be done with an escape
     sequence.  Just like with any other terminal application.

  2. If we are going to support a GUI way of setting the terminal
     name, then it needs to go in the properties, so that the setting
     can be kept across sessions.

Miguel.