bash: Cut long hostname to 5 characters

[dotfiles.git] / .profile

diff --git a/.profile b/.profile
index 2cfb9431d9ad69cb6251fd751ebad263467f4035..07d4f98ced6178296619baaf9824deb83aebf034 100644 (file)
--- a/.profile
+++ b/.profile
@@ -194,7 +194,7 @@ if [ -t 0 ] ; then
 
       if [ -r "$HOME"/admin/prog/short_curdir ]; then
          . "$HOME"/admin/prog/short_curdir
-         OPS1=${OPS1}"${debian_chroot:+($debian_chroot)}\u@\h \`short_curdir\` \\$"
+         OPS1=${OPS1}"${debian_chroot:+($debian_chroot)}\u@\${HOSTNAME::5} \`short_curdir\` \\$"
       else
          OPS1=${OPS1}"${debian_chroot:+($debian_chroot)}\u@\h \W \\$"
       fi