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>