.github/build.sh - use ${xxx##*/} instead of awk as awk may not be installed

awk is not installed on all systems so use bash Remove prefix

 On branch sm-nist
 Changes to be committed:
	modified:   .github/build.sh

Author: dengert

.github/build.sh

@@ -9,14 +9,14 @@ if [ -x "/bin/sudo" ]; then
 fi
 
 if [ "$GITHUB_EVENT_NAME" == "pull_request" ]; then
-	PR_NUMBER=$(echo $GITHUB_REF | awk 'BEGIN { FS = "/" } ; { print $3 }')
+	PR_NUMBER=${GITHUB_REF##*/} 
 	if [ "$GITHUB_BASE_REF" == "master" ]; then
 		SUFFIX="-pr$PR_NUMBER"
 	else
 		SUFFIX="$GITHUB_BASE_REF-pr$PR_NUMBER"
 	fi
 else
-	BRANCH=$(echo $GITHUB_REF | awk 'BEGIN { FS = "/" } ; { print $3 }')
+	BRANCH=$${GITHUB_REF##*/}
 	if [ "$BRANCH" != "master" ]; then
 		SUFFIX="$BRANCH"
 	fi