Try hard resetting the git repo to fix issues with pulling

2024-06-25 14:48:17 +02:00
parent 97e9fe668a
commit 795bc77207
1 changed files with 7 additions and 0 deletions
@@ -104,6 +104,13 @@ git_build_into(){
    fi
  done

+  if [ "$gitterm" -ne 0 ]; then
+    debug "Three git pulls failed, hard resetting and repulling"
+    git -C "$basedir" reset --hard HEAD~50 >"$GITchanges" 2>"$GITerrors"
+    git -C "$basedir" pull >>"$GITchanges" 2>>"$GITerrors"
+    gitterm="$?"
+  fi
+
  if [ "$gitterm" -ne 0 ]; then
    die "GIT reported the following problem:\n$(cat "$GITerrors")"
  fi