From 795bc7720730d7660e2906d2c00190ed60f9050c Mon Sep 17 00:00:00 2001 From: Darragh Elliott Date: Tue, 25 Jun 2024 14:48:17 +0200 Subject: [PATCH] Try hard resetting the git repo to fix issues with pulling --- build/buildrun.sh | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/build/buildrun.sh b/build/buildrun.sh index 03498e407e..a1f0effdcc 100755 --- a/build/buildrun.sh +++ b/build/buildrun.sh @@ -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