Re: gnome-terminal profiles improvement

[Bastien Nocera <hadess hadess net>]

On Tue, 2011-11-15 at 13:56 +0100, Julien Blanc wrote:
> Hi,
> 
> First of all, i apologize if it's not the good list to discuss about this,
> but i couldn’t find a list more specifically related to gnome-terminal
> features.

Patches should be sent to http://bugzilla.gnome.org

> I find current gnome-terminal profiles useful, but in a certain way
> limited. I often have a lot of shells open, logged on different servers
> and/or with different accounts. I used to have different launchers for
> this, but that doesn’t fit well with the new gnome-shell interface, and
> does not handle all cases (i sometimes need to log in a first server to
> access a second one or become root on this server, or tend to prefer to
> reuse an open terminal rather than closing it and opening a new one). So
> I'd like to have one profile per server, and the good one automatically
> selected.
> 
> Thus, i patched gnome-terminal to allow « automagic profile selection ».
> The selection scheme is quite simple : if the xterm-title string matches a
> profile-specific one, then switch to this profile.


For such a feature, I would expect the bug entry to be a good enough
forum to discuss it.

> This is very handy because it is really easy to modify PROMPT_COMMAND to
> set the title, and it is common to use "login@server: PATH". By matching
> login@server, the good profile is automatically selected whenever i log on
> a new server or change my account on this server, and unselected when i
> log off. Different profiles are really easily identified on the activities
> view.
> 
> So, my questions are :
> - is the community interested in such a feature ? (googling around tend to
> show that demand for such a functionality exists, albeit not being very
> common)
> - if so, who do i need to send my patch to ?
> - what would the ui look like (for now, i only implemented the profile
> switching functionality and use gconf-editor to alter the profiles, which
> is enough for me).

Cheers