Maintenance: Improve sync-to-github script.

script/build/sync_repo.sh

@@ -4,6 +4,8 @@ set -ex
 
 GITHUB_DEST=$1
 
+git remote prune origin
+
 if echo $CI_BUILD_REF_NAME | grep private; then
   echo 'sync no private branches'
   exit 0
@@ -21,7 +23,7 @@ fi
 
 git checkout $CI_BUILD_REF_NAME
 if [ "$CI_BUILD_REF_NAME" != "$CI_BUILD_TAG" ]; then
-  git pull --rebase origin $CI_BUILD_REF_NAME
+  git reset --hard origin/$CI_BUILD_REF_NAME
 fi
 
 if git remote | grep github > /dev/null; then
@@ -30,7 +32,7 @@ fi
 git remote add github $GITHUB_DEST
 
 if [ "$CI_BUILD_REF_NAME" != "$CI_BUILD_TAG" ]; then
-  git push github $CI_BUILD_REF_NAME
+  git push -f github $CI_BUILD_REF_NAME
 else
   git push github --tags
 fi