Subject: Re: how do I resolve this merge manually + mergetool bug

From: Junio C Hamano <[email-masked]>
Date: Mon, 23 Feb 2009 23:16:16 -0800

Caleb Cushing <[email-masked]> writes:

> git rm profiles/package.mask
>
> rm 'profiles/package.mask'
> rm 'profiles/package.mask'
> rm 'profiles/package.mask/gentoo.org'

Ahh, ok, "git rm" Porcelain may well be buggy; I almost never use it
myself.

"git update-index --force-remove profiles/package.mask" should work
better.  I tend to trust plumbing a lot more than Porcelain for these
corner cases.