From 43d2a8d26efaa0d1c583ee93fa77643c713d9024 Mon Sep 17 00:00:00 2001
From: Eli Barzilay <eli@barzilay.org>
Date: Tue, 30 Jan 2018 14:47:24 -0500
Subject: [PATCH] Fix checking BUILDPR

(Remove the regexp which I didn't actually use.)
---
 tools/build-pr/shared.sh | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

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: <user>/<repo>/<branch>
-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 "<user>/<repo>/<branch>"
+if [[ "$BUILDPR" != */*/* && "$BUILDPR" = *[^0-9]* ]]; then
   failwith "\$BUILDPR should be a number, got: \"$BUILDPR\""
 fi