1
#!/bin/bash #-- not used anyhow
3
# $Id: file5,v 1.1 2003/12/29 01:56:32 blais Exp $
6
# echo "Bashrc executed"
11
# Reset environment in bash if requested. The reason why we do this is for
12
# setting stuff that depends on the calling process environment, e.g. with
15
if [ -f "$HOME/.cache.bashenv" ]; then
16
# echo "Resetting environment in .bashrc"
17
. $HOME/the-config/.env.pre
18
. $HOME/the-config/.env.scopes
19
. $HOME/the-config/.env.post
22
# check for cache first
23
if [ ! -f "$HOME/.cache.disable" -a \
24
-f "$HOME/.cache.bashrc.$SITE.$PLAT.$HOST" ]; then
26
echo "Using cached .bashrc";
27
. $HOME/.cache.bashrc.$SITE.$PLAT.$HOST
31
#---------------------------------------------------------------------------
32
# source scope-specific bashrc's
34
if [ -f $HOME/the-config/share/.bashrc.local ]; then
35
. $HOME/the-config/share/.bashrc.local
38
if [ -f $HOME/the-config/site/$SITE/.bashrc.local ]; then
39
. $HOME/the-config/site/$SITE/.bashrc.local
42
if [ -f $HOME/the-config/plat/$PLAT/.bashrc.local ]; then
43
. $HOME/the-config/plat/$PLAT/.bashrc.local
46
if [ -f $HOME/the-config/host/$HOST/.bashrc.local ]; then
47
. $HOME/the-config/host/$HOST/.bashrc.local
50
if [ -f $HOME/the-config/site/$SITE/plat/$PLAT/.bashrc.local ]; then
51
. $HOME/the-config/site/$SITE/plat/$PLAT/.bashrc.local
54
if [ -f $HOME/the-config/host/$HOST/plat/$PLAT/.bashrc.local ]; then
55
. $HOME/the-config/host/$HOST/plat/$PLAT/.bashrc.local