From: Junio C Hamano <gitster@pobox.com>
Date: Tue, 24 Feb 2009 07:16:16 GMT
Subject: Re: how do I resolve this merge manually + mergetool bug
Message-ID: <7vr61ol2yn.fsf@gitster.siamese.dyndns.org>
In-Reply-To: <81bfc67a0902232252h56570308r22872854af8da54a@mail.gmail.com>

Caleb Cushing <xenoterracide@gmail.com> 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.