diff --git a/tools/build-pr/shared.sh b/tools/build-pr/shared.sh index 0aeb9219f2..3223abf51d 100644 --- a/tools/build-pr/shared.sh +++ b/tools/build-pr/shared.sh @@ -5,13 +5,8 @@ set -e cd "$BASEDIR" -# For private builds: // -privatebuildrx="([^a-zA-Z0-9][^a-zA-Z0-9-]*)" -privatebuildrx+="/([a-zA-Z0-9+-]+)/([a-zA-Z0-9/+-]+)" - -if [[ "$BUILDPR" = "" ]]; then : -elif [[ "$BUILDPR" =~ $privatebuildrx ]]; then : -elif [[ "$BUILDPR" = *[^0-9]* ]]; then +# BUILDPR can be empty, a PR number, or "//" +if [[ "$BUILDPR" != */*/* && "$BUILDPR" = *[^0-9]* ]]; then failwith "\$BUILDPR should be a number, got: \"$BUILDPR\"" fi