mirror of https://github.com/zulip/zulip.git
push-to-pull-request: Broaden one error message.
I discovered this case just now while testing other changes.
This commit is contained in:
parent
954c71e90c
commit
f686d55fa0
|
@ -57,11 +57,15 @@ if [ "$(pr_jq -r .message)" = "Not Found" ]; then
|
||||||
fi
|
fi
|
||||||
|
|
||||||
if [ "$(pr_jq .maintainer_can_modify)" != "true" ]; then
|
if [ "$(pr_jq .maintainer_can_modify)" != "true" ]; then
|
||||||
# This seems to be rare (in Greg's experience doing the manual
|
# This happens when the PR has already been merged or closed, or
|
||||||
# equivalent of this script for many different contributors, none
|
# if the contributor has turned off the (default) setting to allow
|
||||||
# have ever chosen this setting), but give a decent error message
|
# maintainers of the target repo to push to their PR branch.
|
||||||
# if it does happen.
|
#
|
||||||
echo "error: contributor has disallowed pushing to PR branch" >&2
|
# The latter seems to be rare (in Greg's experience doing the
|
||||||
|
# manual equivalent of this script for many different
|
||||||
|
# contributors, none have ever chosen this setting), but give a
|
||||||
|
# decent error message if it does happen.
|
||||||
|
echo "error: PR already closed, or contributor has disallowed pushing to branch" >&2
|
||||||
exit 1
|
exit 1
|
||||||
fi
|
fi
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue