Skip to content

Instantly share code, notes, and snippets.

@anujonthemove
Created December 30, 2021 04:09
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save anujonthemove/185ccd982b63e224a85f37db9b60c485 to your computer and use it in GitHub Desktop.
Save anujonthemove/185ccd982b63e224a85f37db9b60c485 to your computer and use it in GitHub Desktop.
Rename terminal tab on Ubuntu 20.x
# directly taken from: https://unix.stackexchange.com/questions/177572/how-to-rename-terminal-tab-title-in-gnome-terminal
function set-title() {
if [[ -z "$ORIG" ]]; then
ORIG=$PS1
fi
TITLE="\[\e]2;$*\a\]"
PS1=${ORIG}${TITLE}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment