From 7be0dbfbed31197cb7fdad141d3658064f81c2f9 Mon Sep 17 00:00:00 2001
From: Giacomo Tesio <giacomo@tesio.it>
Date: Thu, 19 Jan 2017 19:26:21 +0100
Subject: [PATCH] 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
---
 devshell.sh | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/devshell.sh b/devshell.sh
index 4558698..f46d5a8 100755
--- a/devshell.sh
+++ b/devshell.sh
@@ -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"')