The command "git checkout" checks out from the index by default, not
HEAD (the introducing comment were correct, but the detailled
explanation added below were not).
Signed-off-by: Matthieu Moy <Matthieu.Moy@imag.fr> Signed-off-by: Junio C Hamano <gitster@pobox.com>