From 84bbf984d04e5395d498d0ed690a1011db44bbfd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20P=C3=A9pin?= <martin.pepin@ens.fr>
Date: Tue, 16 May 2017 22:00:00 +0100
Subject: [PATCH] Avoid duplicate lines in .bash{rc,_profile}

---
 provisioning/bootstrap.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/provisioning/bootstrap.sh b/provisioning/bootstrap.sh
index 2cbda4b..15f76d6 100644
--- a/provisioning/bootstrap.sh
+++ b/provisioning/bootstrap.sh
@@ -109,7 +109,9 @@ venv_python manage.py migrate
 # Setup a friendly environment for the user
 # ---
 
-cat >> ~vagrant/.bashrc <<EOF
+cat > ~vagrant/.bash_profile <<EOF
+# Use the .bashrc file provided by Debian
+source .bashrc
 
 # Use the development settings
 export DJANGO_SETTINGS_MODULE="$SETTINGS"