Wladimir J. van der Laan 3802ae7267 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.

2015-09-18 06:03:17 +02:00

5.4 KiB

Executable File

Raw Blame History

View Raw