aboutsummaryrefslogtreecommitdiff
path: root/contrib/devtools/github-merge.sh
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/devtools/github-merge.sh')
-rwxr-xr-xcontrib/devtools/github-merge.sh18
1 files changed, 15 insertions, 3 deletions
diff --git a/contrib/devtools/github-merge.sh b/contrib/devtools/github-merge.sh
index 3217a06195..afb53f0390 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
@@ -153,12 +156,21 @@ read -p "Press 's' to sign off on the merge. " -n 1 -r >&2
echo
if [[ "d$REPLY" =~ ^d[Ss]$ ]]; then
if [[ "$(git config --get user.signingkey)" == "" ]]; then
- echo "WARNING: No GPG signing key set, not signing. Set one using:" >&2
+ echo "ERROR: No GPG signing key set, not signing. Set one using:" >&2
echo "git config --global user.signingkey <key>" >&2
- git commit -q --signoff --amend --no-edit
+ cleanup
+ exit 1
else
- git commit -q --gpg-sign --amend --no-edit
+ if ! git commit -q --gpg-sign --amend --no-edit; then
+ echo "Error signing, exiting."
+ cleanup
+ exit 1
+ fi
fi
+else
+ echo "Not signing off on merge, exiting."
+ cleanup
+ exit 1
fi
# Clean up temporary branches, and put the result in $BRANCH.