Maintenance: refactor push to github CI job.

script/build/sync_repo.sh

@@ -4,25 +4,30 @@ set -ex
 
 GITHUB_DEST=$1
 
-git remote prune origin
-
-if echo $CI_BUILD_REF_NAME | grep -E "^(private|cherry-pick-|renovate/|dependabot/)"; then
-  echo 'Do not sync internal branches.'
+# This can be called for branches or tags. Filter out private branches first.
+if [[ $CI_COMMIT_BRANCH =~ ^(private|cherry-pick-|renovate/|dependabot/) ]]
+then
+  echo "Do not sync internal branch ${CI_COMMIT_BRANCH}."
   exit 0
 fi
 
-git checkout $CI_BUILD_REF_NAME
-if [ "$CI_BUILD_REF_NAME" != "$CI_BUILD_TAG" ]; then
-  git reset --hard origin/$CI_BUILD_REF_NAME
-fi
+# Keep things tidy.
+git remote prune origin
 
-if git remote | grep github > /dev/null; then
+# Make sure github remote is up-to-date.
+if git remote | grep github > /dev/null
+then
   git remote rm github
 fi
-git remote add github $GITHUB_DEST
+git remote add github "$GITHUB_DEST"
 
-if [ "$CI_BUILD_REF_NAME" != "$CI_BUILD_TAG" ]; then
-  git push -f github $CI_BUILD_REF_NAME
+if [ "$CI_COMMIT_BRANCH" ]
+then
+  # Commit
+  git checkout "$CI_COMMIT_BRANCH"
+  git reset --hard origin/"$CI_COMMIT_BRANCH"
+  git push -f github "$CI_COMMIT_BRANCH"
 else
+  # Tag
   git push github --tags
 fi