Fix a misbehavior of git #4998

#4998

.github/workflows/mirror.yaml

@@ -24,10 +24,18 @@ jobs:
     - name: Mirror
       run: |
         export GIT_SSH_COMMAND="ssh -v -i ~/.ssh/id_ed25519"
-        git remote add mirror [email protected]:oursky/authgear-server.git
-        git push --tags --force --prune mirror "refs/remotes/origin/*:refs/heads/*"
+        # The original command is
+        #    git push --tags --force --prune "[email protected]:oursky/authgear-server.git" "refs/remotes/origin/*:refs/heads/*"
+        #
+        # It has been working so well, until 2025-01-23, git starts include refs/remotes/origin/HEAD in the expansion.
+        # That would include refs/remotes/origin/HEAD:refs/heads/HEAD.
+        # That means push a branch named HEAD in the mirror repository.
+        # HEAD has a special meaning in Git, and it is obviously not suitable for a branch name.
+        #
+        # So we use `git show-ref` plus some filtering with awk and perl to filter out refs/remotes/origin/HEAD.
+        # And build the `git push ...` command with xargs.
+        git show-ref | awk '{ print $2 }' | perl -n -e 'if (/(^refs\/remotes\/origin\/(.+)$)/ ) { if ($2 != "HEAD") {  print "$1:refs/heads/$2\n" } }' | xargs -x git push --tags --force --prune "[email protected]:oursky/authgear-server.git"
     - name: Clean up
       if: ${{ always() }}
       run: |
         rm -f ~/.ssh/id_ed25519
-        git remote remove mirror