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.
This commit is contained in:
Willy Tarreau 2025-10-08 04:35:52 +02:00
parent 45fba1db27
commit f657ffc6e7

View File

@ -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' ')