From 84e1a34d8cc3838b7666ba26f02648cdee4906c6 Mon Sep 17 00:00:00 2001
From: Iain Patterson <me@iain.cx>
Date: Fri, 26 Sep 2014 09:39:59 +0100
Subject: [PATCH] Shortcut to setting PROFILE_HOME.

Allow sourcing .bash_profile directly to set up PROFILE_HOME.

A user can now simply run ``. /profile/path/.bash_profile'' instead of
``PROFILE_HOME=/profile/path; .  $PROFILE_HOME/.bash_profile'' to use
these scripts.
---
 .bash_profile | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/.bash_profile b/.bash_profile
index 6fe0759..3d5d075 100644
--- a/.bash_profile
+++ b/.bash_profile
@@ -1,4 +1,13 @@
 if [ -t 0 -o "${0:0:1}" = "-" -o "$1" = "force" ]; then
+  # Set up PROFILE_HOME if called outside HOME.
+  if [ -z "$PROFILE_HOME" ]; then
+    # BASH_SOURCE isn't available prior to bash 3.
+    profile_home=${BASH_SOURCE%/*}
+    [ "$profile_home" = "$BASH_SOURCE" ] && profile_home=$PWD
+    [ "$profile_home" = "$HOME" ] || PROFILE_HOME=$profile_home
+    unset profile_home
+  fi
+
   # Remember if nocaseglob was on.
   shopt -q nocaseglob
   nocg=$?
-- 
2.20.1