From 16aea5ed1de79a99447db48c0ee14c060b1f806c Mon Sep 17 00:00:00 2001
From: short <>
Date: Tue, 9 Oct 2001 21:56:57 +0000
Subject: [PATCH] $HOME/.bash_profile.local is now also optionally executed

---
 .bash_profile | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.bash_profile b/.bash_profile
index 9808136..d5f43d7 100644
--- 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
-- 
1.8.3.1