Re: HEAD branch duplicated in remotes/origin

> Uwe Zeisberger <zeisberg@informatik.uni-freiburg.de> writes:
> 
> > when cloning with --use-separate-remote, $GITDIR/remotes/origin contains
> > two references to refs/heads/master.
> 
> Thanks for noticing.
> 
> Very lightly tested but I think this should fix it.
> -- >8 --
> git-clone: fix duplicated "master" in $GIT_DIR/remotes/origin
> 
> Under --use-separate-remote we ended up duplicating the branch
> remote HEAD pointed at in $GIT_DIR/remotes/origin file.
> 
> Signed-off-by: Junio C Hamano <junkio@cox.net>
> ---
> diff --git a/git-clone.sh b/git-clone.sh
> index de59904..64318b4 100755
> --- a/git-clone.sh
> +++ b/git-clone.sh
> @@ -391,11 +391,16 @@ Pull: refs/heads/$head_points_at:$origin
>  		(cd "$GIT_DIR/$remote_top" && find . -type f -print) |
>  		while read dotslref
>  		do
> -			name=`expr "$dotslref" : './\(.*\)'` &&
> -			test "$use_separate_remote" = '' && {
> -				test "$head_points_at" = "$name" ||
> -				test "$origin" = "$name"
> -			} ||
> +			name=`expr "$dotslref" : './\(.*\)'`
> +			if test "z$head_points_at" = "z$name"
> +			then
> +				continue
> +			fi
> +			if test "$use_separate_remote" = '' &&
> +			   test "z$origin" = "z$name"
> +			then
> +				continue
> +			fi
>  			echo "Pull: refs/heads/${name}:$remote_top/${name}"
>  		done >>"$GIT_DIR/remotes/$origin" &&
>  		case "$use_separate_remote" in
>