Backport #32075 by @lunny After migrating a repository with pull request, the branch is missed and after the pull request merged, the branch cannot be deleted. Co-authored-by: Lunny Xiao <xiaolunwen@gmail.com>
revive
git push --tags --force