user/bash_profile: don't forget to read /etc/profile

diff --git a/user/bash_profile b/user/bash_profile
index a01661385e077407998b1358f57e4d41cf3b5bad..0c0eded6bed469b4bad98307234de18302953078 100644 (file)
--- a/user/bash_profile
+++ b/user/bash_profile
@@ -13,6 +13,7 @@
 [ -e ~/.ConfigScripts.debug ] && echo " .. ~/.bash_profile ..."
 
 [ -z "$PROFILEREAD" -a -r ~/.etc/profile ] && source ~/.etc/profile
+[ -z "$PROFILEREAD" -a -r /etc/profile ] && source /etc/profile
 [ -r ~/.bash_profile.user ] && source ~/.bash_profile.user
 
 [ -e ~/.ConfigScripts.debug ] && echo " >> ~/.bash_profile ..."