Skip to content

Commit

Permalink
Merge pull request #6692
Browse files Browse the repository at this point in the history
3802ae7 devtools: don't push if signing fails in github-merge (Wladimir J. van der Laan)
  • Loading branch information
laanwj committed Sep 18, 2015
2 parents 8bc1b3a + 3802ae7 commit d5d1d2e
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion contrib/devtools/github-merge.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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."
Expand Down

0 comments on commit d5d1d2e

Please sign in to comment.