Browse Source

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.
0.13
Wladimir J. van der Laan 9 years ago
parent
commit
3802ae7267
  1. 6
      contrib/devtools/github-merge.sh

6
contrib/devtools/github-merge.sh

@ -161,7 +161,11 @@ if [[ "d$REPLY" =~ ^d[Ss]$ ]]; then @@ -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."

Loading…
Cancel
Save