git-checkout: allow "checkout HEAD -- path"

Even though -- is redundant in this case, we should allow it to prevent
confusion.

Signed-off-by: Junio C Hamano <junkio@cox.net>

diff --git a/git-checkout.sh b/git-checkout.sh
index 5613bfc403f7a4208d2a85de73ec33229e5a3f10..580a9e8a233f0a94c84792eba7c3dc653fccf3a0 100755 (executable)
--- a/git-checkout.sh
+++ b/git-checkout.sh
@@ -67,6 +67,10 @@ while [ "$#" != "0" ]; do
                        set x "$arg" "$@"
                        shift
                fi
+               case "$1" in
+               --)
+                       shift ;;
+               esac
                break
                ;;
     esac