Changer le titre d'un onglet gnome terminal

[Damien POBEL]

Salut,

Daniel C a écrit :
> Romain Thouvenin wrote:
>> C'est étrange, car chez moi, quand je change d'host avec une
>> connection ssh, le nom de l'onglet change aussi... Peut être que cela
>> se configure ?
> 
> Ca devrait être dans le profil, mais j'ai bien le choix "remplacer le titre" pour l'option "un titre modifié dynamiquement" de l'onglet "titre et 
> commande", mais je reste toujours avec mon user at host initial dans l'onglet, même si le prompt change au gré des connexions ssh...
je crois plutôt que c'est au niveau de la configuration du shell sur le serveur 
que ça passe. Personnellenement pour avoir ce genre de comportement, j'ai ces 
quelques lignes dans mes .bashrc  :

case $TERM in
   xterm*)
     PROMPT_COMMAND='echo -ne "\033]0;${USER}@${MACHINE}[$IP]: ${PWD}\007"'
     echo -ne "\033]0;${USER}@${MACHINE}[$IP]: ${PWD}\007"
         ;;
     *)
         ;;
     esac

Le echo -ne "\0033]0; un chaine \007" permet de changer dynamiquement le titre. 
Et PROMPT_COMMAND est un variable que bash tente d'éxécuter à chaque fois qu'il 
affiche le prompt.

-- 
Damien POBEL <dpobel at free.fr>
http://pwet.fr/blog