diff options
Diffstat (limited to 'local/require-signed-push')
| -rwxr-xr-x | local/require-signed-push | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/local/require-signed-push b/local/require-signed-push index eef887b..f2d6e8e 100755 --- a/local/require-signed-push +++ b/local/require-signed-push @@ -157,7 +157,7 @@ case ${VERIFY_SIGS} in if [[ ${GL_USER} != *@gentoo.org ]]; then warn "*** Pusher address is not @gentoo.org" >&2 warn " (it is ${GL_USER})" >&2 - warn "*** Please report this to infra" >&2 + warn "*** Please report this to infra ($0)" >&2 silent_die fi |