From 484bec440aeb51ed85952be3bdde036399ff99c8 Mon Sep 17 00:00:00 2001
From: David Tucker <david.tucker@emc.com>
Date: Wed, 26 Aug 2026 17:18:11 -0700
Subject: [PATCH] Use $HOME for sourcing bashrc.bash

Make sharing .bashrc on machines with different homes a little smoother.
---
 install/bash.bash | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/install/bash.bash b/install/bash.bash
index ec71ed9..a092bb7 100644
--- a/install/bash.bash
+++ b/install/bash.bash
@@ -17,7 +17,7 @@ cp -v "$config_repo/config/$(basename "$config_bashrc")" "$config_bashrc"
 echo "rm '$config_bashrc'" >> "$config_undo"
 
 signature='# added by dmtucker/config'
-source_config="source '$config_bashrc'"
+source_config="source \"${config_bashrc/#$HOME/\$HOME}\""
 bashrc="$(realpath "$HOME/.bashrc")"
 grep -q "$source_config" "$bashrc" || {
     echo "sed -i '\|$signature|d' '$bashrc'" >> "$config_undo"