Fix switch to another git branch (#202)

Windows-on-ARM-Experiments · Oct 10, 2024 · 4c04dbe · 4c04dbe
1 parent d897fe5
commit 4c04dbe
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/.github/scripts/update-sources.sh b/.github/scripts/update-sources.sh
@@ -17,6 +17,10 @@ function update_repository() {
         pushd $DIRECTORY
             if [[ "$RESET_SOURCES" = 1 ]]; then
                 git reset --hard HEAD
+                if ! git show-ref --verify --quiet refs/remotes/origin/$BRANCH; then
+                    git remote set-branches --add origin $BRANCH
+                    git fetch origin --prune
+                fi
                 git switch $BRANCH
                 git clean -fdx
             fi