diff options
| author | Kévin Le Gouguec <kevin.legouguec@gmail.com> | 2021-04-27 22:52:25 +0200 |
|---|---|---|
| committer | Kévin Le Gouguec <kevin.legouguec@gmail.com> | 2021-04-27 22:52:25 +0200 |
| commit | 5ac43c1b2a921fd2745f0d9945279f14c240ae89 (patch) | |
| tree | ae3a7b57147a7babfbf5ee37ff2db7f8e49005ff | |
| parent | ce9b3d4d27268e5123535f348ea3f0f8f553f972 (diff) | |
| download | dotfiles-5ac43c1b2a921fd2745f0d9945279f14c240ae89.tar.xz | |
Tweak window title for terminal emulators
| -rw-r--r-- | .bash_prompt | 25 |
1 files changed, 16 insertions, 9 deletions
diff --git a/.bash_prompt b/.bash_prompt index a922033..9b753b3 100644 --- a/.bash_prompt +++ b/.bash_prompt @@ -25,20 +25,27 @@ __have-gitprompt () __set-title () { - local title - local git_root=$(git root 2> /dev/null) + local title=${USER} + if __show-hostname + then + title+="@${HOSTNAME}" + fi + title+=: - if [ ${git_root} ] + local path=${PWD/~/\~} + local git_root=$(git rev-parse --show-toplevel 2> /dev/null) + + if [ -z "${git_root}" -o "${git_root}" = ~ ] then - title=$(basename ${git_root}) + title+=${path} else - local path=${PWD/~/\~} - - if __show-hostname + local project=$(basename "${git_root}") + path=$(realpath --relative-to "${git_root}" "${PWD}") + if [ "${path}" = . ] then - title="${USER}@${HOSTNAME}:${path}" + title+=${project} else - title="${USER}:${path}" + title+=${project}/${path} fi fi |