diff options
| -rwxr-xr-x | local/require-signed-push | 2 | ||||
| -rwxr-xr-x | local/update-02-gpg | 2 |
2 files changed, 2 insertions, 2 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 diff --git a/local/update-02-gpg b/local/update-02-gpg index b0dc1b1..ffae5cf 100755 --- a/local/update-02-gpg +++ b/local/update-02-gpg @@ -30,7 +30,7 @@ case ${VERIFY_SIGS} in if [[ ${GL_USER} != *@gentoo.org ]]; then echo "*** Pusher address is not @gentoo.org" >&2 echo " (it is ${GL_USER})" >&2 - echo "*** Please report this to infra" >&2 + echo "*** Please report this to infra ($0)" >&2 exit 1 fi |