¿Cómo cambiar el nombre del título de la pestaña del terminal en gnome-terminal?

¿Cómo cambiar el nombre del título de la pestaña del terminal en gnome-terminal?

Solía ​​​​poder hacer clic derecho en la pestaña y cambiar el título. Ya no estoy seguro de cómo hacer esto. Recién actualizado a Fedora 21.

EDITAR: He cambiado de gnome-terminal a ROXterm

Respuesta1

Crea una función en ~/.bashrc:

function set-title() {
  if [[ -z "$ORIG" ]]; then
    ORIG=$PS1
  fi
  TITLE="\[\e]2;$*\a\]"
  PS1=${ORIG}${TITLE}
}

Luego use su nuevo comando para configurar el título del terminal. También funciona con espacios en el nombre.

set-title my new tab title

Es posible set-titlevolver a utilizarlo posteriormente (la PS1 original se conserva como ORIG).

Respuesta2

El user titlecódigo fue eliminado 1 de gnome-terminal 3.14. Para establecer el título, puede utilizar una secuencia de escape:

printf "\e]2;YOUR TITLE GOES HERE\a"

o por ejemplo con bash:

echo -ne "\033]0;YOUR TITLE GOES HERE\007"

Argumentos -nepara echono agregar un carácter de nueva línea e interpretar secuencias de escape (como \033).


1: ver gnomoerror 724110y gnomoerror 740188.

Respuesta3

Las nuevas versiones de gnome-terminal simplemente eliminan las funciones profesionales más útiles. :-(

Intenté configurar y ejecutar una versión anterior de gnome-terminal y también comparé alternativas.

Si terminatorte parece demasiado exótico, ¡ mate-terminales una gran opción! Es una bifurcación de gnome-terminal y simplemente mantiene todas las buenas características:

  • puedes abrir varias pestañas desde la línea de comando dándoles diferentes títulos

    mate-terminal --tab -t "aaa" --tab -t "bbb" --tab -t "ccc"
    
  • puedes configurar un atajo de teclado (yo uso Ctrl+Shift-i) para establecer enitítulo

Respuesta4

Si está utilizando Ubuntu 16.04, es posible que necesite:

PS1=$
PROMPT_COMMAND=
echo -en "\033]0;New title\a"

Enumero esto y más información al respecto enenlace.

información relacionada