$HOME/.bash_profile.local is now also optionally executed

diff --git a/.bash_profile b/.bash_profile
index 9808136..d5f43d7 100644 (file)
--- a/.bash_profile
+++ b/.bash_profile
@@ -2,3 +2,5 @@ if [ -f "$HOME/.bashrc" ];then export BASH_ENV="$HOME/.bashrc";source "$BASH_ENV
 
 finger
 m
+
+if [ -f "$HOME/.bash_profile.local" ];then source "$HOME/.bash_profile.local";fi