From 655f5c2fb452c793d9d7c994e2867358c3b38cd4 Mon Sep 17 00:00:00 2001
From: Midgard <midgard@zeus.ugent.be>
Date: Sat, 21 May 2022 01:43:42 +0200
Subject: [PATCH] Never push "HEAD"; don't touch current branch

---
 git-mirror.sh | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/git-mirror.sh b/git-mirror.sh
index 4e48474..81dab19 100755
--- a/git-mirror.sh
+++ b/git-mirror.sh
@@ -81,6 +81,7 @@ for branchspec in "${branches[@]}"; do
 	set $branchspec
 	leader_sha="$1"
 	branch="$2"
+	if [ "$branch" = HEAD ]; then continue; fi
 
 	for remote in "${followers[@]}"; do
 		echo
@@ -90,7 +91,7 @@ for branchspec in "${branches[@]}"; do
 
 		if ! ref_exists "$follower_ref"; then
 			echo "Branch doesn't yet exist at remote, creating"
-			git reset --hard "$leader_sha" --
+			git checkout "$leader_sha" --
 			git push "$remote" "+HEAD:$branch" || { error "$remote $branch: failed to push"; continue; }
 
 		elif is_ref_at_sha "$follower_ref" "$leader_sha"; then
@@ -98,7 +99,7 @@ for branchspec in "${branches[@]}"; do
 
 		else
 			echo "Branch exists at remote, updating"
-			git reset --hard "$follower_ref" --
+			git checkout "$follower_ref" --
 			git merge --ff-only "$leader_sha" || { error "$remote $branch: FF not possible"; continue; }
 			git push "$remote" "+HEAD:$branch" || { error "$remote $branch: failed to push"; continue; }
 		fi