From 3802ae72670faf46c96d0f5f262e42cae92c5a42 Mon Sep 17 00:00:00 2001
From: "Wladimir J. van der Laan" <laanwj@gmail.com>
Date: Fri, 18 Sep 2015 06:03:17 +0200
Subject: [PATCH] devtools: don't push if signing fails in github-merge

If a problem happens with gpg, exit prematurely so that it doesn't push
the branch upstream.
---
 contrib/devtools/github-merge.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/contrib/devtools/github-merge.sh b/contrib/devtools/github-merge.sh
index ec7a1f4c4b..afb53f0390 100755
--- a/contrib/devtools/github-merge.sh
+++ b/contrib/devtools/github-merge.sh
@@ -161,7 +161,11 @@ if [[ "d$REPLY" =~ ^d[Ss]$ ]]; then
     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."