aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorWladimir J. van der Laan <laanwj@gmail.com>2014-12-09 15:33:58 +0100
committerWladimir J. van der Laan <laanwj@gmail.com>2014-12-09 15:34:02 +0100
commit0a1d03ca5265293e6419b0ffb68d277da6b1d9a0 (patch)
treea5b3c2dba5815306d3d32df4b22ba5d398457aac
parent09ac7f9e6d3f4d57453e9c54f376eb67f035a86c (diff)
parent6e6a36ce308ae81529027b6e18f7ba1aeabe8dd7 (diff)
downloadbitcoin-0a1d03ca5265293e6419b0ffb68d277da6b1d9a0.tar.xz
Merge pull request #5449
6e6a36c contrib: show pull # in prompt for github-merge script (Wladimir J. van der Laan)
-rwxr-xr-xcontrib/devtools/github-merge.sh3
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/devtools/github-merge.sh b/contrib/devtools/github-merge.sh
index 3217a06195..6f68496ed8 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