DEV: patchbot: use git reset+checkout instead of pull

The patchbot stopped on a previous ultra-rare forced push due to wanting
the user's name and e-mail before proceeding. We don't want merges nor
rebases anyway, only to reset the tree to the next one, so let's do that.

diff --git a/dev/patchbot/scripts/update-3.0.sh b/dev/patchbot/scripts/update-3.0.sh
index 5f8ac87b406f4131458827b680bc935bf5fce31f..b661f26cb62be7986fdb47a554f61d42b6733462 100755 (executable)
--- a/dev/patchbot/scripts/update-3.0.sh
+++ b/dev/patchbot/scripts/update-3.0.sh
@@ -22,7 +22,8 @@ STABLE=$(cd "$HAPROXY_DIR" && git describe --tags "v${BRANCH}-dev0^" |cut -f1,2
 PATCHES_DIR="$PATCHES_PFX"-"$BRANCH"
 
 (cd "$HAPROXY_DIR"
- git pull
+ # avoid git pull, it chokes on forced push
+ git remote update origin; git reset origin/master;git checkout -f
  last_file=$(ls -1 "$PATCHES_DIR"/*.patch 2>/dev/null | tail -n1)
  if [ -n "$last_file" ]; then
        restart=$(head -n1 "$last_file" | cut -f2 -d' ')