From 6e6a36ce308ae81529027b6e18f7ba1aeabe8dd7 Mon Sep 17 00:00:00 2001
From: "Wladimir J. van der Laan" <laanwj@gmail.com>
Date: Tue, 9 Dec 2014 10:16:58 +0100
Subject: [PATCH] contrib: show pull # in prompt for github-merge script

---
 contrib/devtools/github-merge.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/contrib/devtools/github-merge.sh b/contrib/devtools/github-merge.sh
index 3217a0619..6f68496ed 100755
--- a/contrib/devtools/github-merge.sh
+++ b/contrib/devtools/github-merge.sh
@@ -136,6 +136,9 @@ else
   echo "Dropping you on a shell so you can try building/testing the merged source." >&2
   echo "Run 'git diff HEAD~' to show the changes being merged." >&2
   echo "Type 'exit' when done." >&2
+  if [[ -f /etc/debian_version ]]; then # Show pull number in prompt on Debian default prompt
+      export debian_chroot="$PULL"
+  fi
   bash -i
   read -p "Press 'm' to accept the merge. " -n 1 -r >&2
   echo