The example to remove paths using index-filter was done with
"git update-index --remove"; "git rm --cached" would be more familiar to
new people and is sufficient for this particular case.
Signed-off-by: Petr Baudis <pasky@suse.cz> Signed-off-by: Junio C Hamano <gitster@pobox.com>