On Mon, Feb 09, 2004 at 01:28:04PM -0500, David Clymer wrote:
>On Mon, 2004-02-09 at 06:57, Magnus Therning wrote:
>> I realize this is slightly off topic here, but it seems a lot of REALLY
>> knowledgable people inhabit this list :-)
>>
>
>Flattery will get you nowhere. Besides, I know you're not talking about
>me ;o)
>
>> Is there a way of switching the profile of a running gnome-terminal,
>> without using the menu? I am mostly interested of doing it from inside
>> the terminal itself.
>>
>> I could imagine it being done via an escape sequence, or a call to an
>> executable, e.g. gnome-terminal, that takes the profile name as an
>> argument. Just as long as I don't need to use the mouse :-)
>>
>
>Is there any particular reason you dont want to use the menus? In gnome
>2.4 (I dont know what version you are using), I can easily switch
>profiles from within gnome-terminal _using_ the menus but without a
>mouse (Alt-T P, arrow keys).
E.g. I have the following settings in my bash:
PROMPT_COMMAND='echo -ne "\033]0;${USER}@${HOSTNAME}: ${PWD}\007"'
and a root chell executes in its bash configuration:
printf "\033]0; ROOT SHELL \007"
This results in XTerms containing a root shell quite visible. However,
they would be even more visible if I could change the profile from
within the configuration files to bash.
/M
--
-----------------------------------------------------------------------
Magnus Therning Philips Research Laboratories Eindhoven
Phone: +31 40 2745179 (OpenPGP: 0x4FBB2C40)
The only way to be truly creative is to never repeat yourself.
-- Rob Breszny
Attachment:
signature.asc
Description: Digital signature