Merge pull request #6692
3802ae7
devtools: don't push if signing fails in github-merge (Wladimir J. van der Laan)
This commit is contained in:
commit
d5d1d2e65a
1 changed files with 5 additions and 1 deletions
|
@ -161,7 +161,11 @@ if [[ "d$REPLY" =~ ^d[Ss]$ ]]; then
|
||||||
cleanup
|
cleanup
|
||||||
exit 1
|
exit 1
|
||||||
else
|
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
|
fi
|
||||||
else
|
else
|
||||||
echo "Not signing off on merge, exiting."
|
echo "Not signing off on merge, exiting."
|
||||||
|
|
Loading…
Reference in a new issue