Vagrant: augment bash when working in a git repository

This .bashrc_git originally came from tridge.

Tools/vagrant/bashrc_git

@@ -0,0 +1,30 @@
+function parse_git_branch {
+  /usr/bin/git branch --no-color 2> /dev/null | sed -e '/^[^*]/d' -e 's/* \(.*\)/(\1)/'
+}
+
+function proml {
+  local      NORMAL="\[\033[0;0m\]"
+  local        BLUE="\[\033[0;34m\]"
+  local       BLACK="\[\033[0;30m\]"
+  local         RED="\[\033[0;31m\]"
+  local   LIGHT_RED="\[\033[1;31m\]"
+  local       GREEN="\[\033[0;32m\]"
+  local LIGHT_GREEN="\[\033[1;32m\]"
+  local       WHITE="\[\033[1;37m\]"
+  local  LIGHT_GRAY="\[\033[0;37m\]"
+  case $TERM in
+    xterm*|screen*)
+    TITLEBAR='\[\033]0;\u@\h:\w\007\]'
+    ;;
+    *)
+    TITLEBAR=""
+    ;;
+  esac
+
+PS1="${TITLEBAR}\
+\u@\h:\w$BLUE\$(parse_git_branch)$NORMAL\\$ "
+PS2='> '
+PS4='+ '
+}
+proml
+

Tools/vagrant/initvagrant-trusty64.sh

@@ -27,6 +27,12 @@ export BUILDLOGS=/tmp/buildlogs
 DOT_PROFILE=/home/$VAGRANT_USER/.profile
 
 echo "$PROFILE_TEXT" | sudo -u $VAGRANT_USER dd conv=notrunc oflag=append of=$DOT_PROFILE
+
+# adjust environment for every login shell:
+BASHRC_GIT="/vagrant/Tools/vagrant/bashrc_git"
+echo "source $BASHRC_GIT" |
+    sudo -u $VAGRANT_USER dd conv=notrunc oflag=append of=$DOT_PROFILE
+
 sudo -u $VAGRANT_USER ln -fs /vagrant/Tools/vagrant/screenrc /home/$VAGRANT_USER/.screenrc
 
 # build JSB sim

Tools/vagrant/initvagrant.sh

@@ -52,6 +52,12 @@ DOT_PROFILE=/home/$VAGRANT_USER/.profile
 echo "source /vagrant/Tools/vagrant/shellinit.sh" |
     sudo -u $VAGRANT_USER dd conv=notrunc oflag=append of=$DOT_PROFILE
 
+BASHRC="/home/$VAGRANT_USER/.bashrc"
+# adjust environment for every login shell:
+BASHRC_GIT="/vagrant/Tools/vagrant/bashrc_git"
+echo "source $BASHRC_GIT" |
+    sudo -u $VAGRANT_USER dd conv=notrunc oflag=append of=$BASHRC
+
 # link a half-way decent .mavinit.scr into place:
 sudo --login -u $VAGRANT_USER ln -sf /vagrant/Tools/vagrant/mavinit.scr /home/$VAGRANT_USER/.mavinit.scr