devshell.sh: introduce $JEHANNE_DEVELOPER_DIR

$JEHANNE_DEVELOPER_DIR (default to ~/.jehanne) can hooks the
into the enviroment started by ./hacking/devshell.sh:

	$JEHANNE_DEVELOPER_DIR/devshell.sh is sourced by ./hacking/devshell.sh
	$JEHANNE_DEVELOPER_DIR/gdbinit is sourced by gdb started with ./hacking/gdb.sh
This commit is contained in:
Giacomo Tesio 2017-01-19 19:26:21 +01:00
parent a14a0f9224
commit 7be0dbfbed
1 changed files with 14 additions and 0 deletions

View File

@ -6,4 +6,18 @@ export ARCH=amd64
export TOOLPREFIX=x86_64-jehanne-
# let each developer to customize her environment
if [ "$JEHANNE_DEVELOPER_DIR" = "" ]; then
JEHANNE_DEVELOPER_DIR=$HOME/.jehanne/
fi
if [ -d "$JEHANNE_DEVELOPER_DIR" ]; then
export JEHANNE_DEVELOPER_DIR
if [ -f "$JEHANNE_DEVELOPER_DIR/devshell.sh" ]; then
if [ "$JEHANNE_DEVELOPER_INIT_RUN" != "1" ]; then
. "$JEHANNE_DEVELOPER_DIR/devshell.sh"
export JEHANNE_DEVELOPER_INIT_RUN=1
fi
fi
fi
bash --rcfile <(cat ~/.bashrc; echo 'PS1="JehanneDEV $PS1"')