Install user/bash_profile as $HOME/.profile, if this file exists

diff --git a/install.sh b/install.sh
index c7e7d257964c96e5bbcc03852b0041d5ce18dc97..2453855bd191972b82d305a8fe10e5e177cff493 100755 (executable)
--- a/install.sh
+++ b/install.sh
@@ -49,7 +49,11 @@ fi
 user=`basename "$HOME"`
 echo "Starting user configuration ($user in $HOME):"
 echo " - bash shell:"
-Copy_File user/bash_profile "$HOME/.bash_profile" "$user" 600
+if [ -e "$HOME/.profile" ]; then
+       Copy_File user/bash_profile "$HOME/.profile" "$user" 600
+else
+       Copy_File user/bash_profile "$HOME/.bash_profile" "$user" 600
+fi
 Copy_File user/bashrc "$HOME/.bashrc" "$user" 600
 Copy_File user/bash_logout "$HOME/.bash_logout" "$user" 600