From 5edfc00f0867b200d657d03920c9caf43ab89b6e Mon Sep 17 00:00:00 2001
From: Alexander Hess <alexander@webartifex.biz>
Date: Wed, 13 Sep 2023 11:52:33 +0200
Subject: [PATCH] Integrate machine-specific ENV variables

~/.profile_local can now be used to define machine-specific ENV
variables and other shell initialization logic.
---
 .profile | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.profile b/.profile
index 1aa420a..2994e9e 100644
--- a/.profile
+++ b/.profile
@@ -78,3 +78,9 @@ if [ -n "$BASH_VERSION" ]; then
         source "$HOME/.bashrc"
     fi
 fi
+
+
+# Source ~/.profile_local, which holds machine-specific ENV variables
+if [ -f "$HOME/.profile_local" ]; then
+    source "$HOME/.profile_local"
+fi