Re: [PATCH] Demonstrate failure of 'core.ignorecase = true'

[Jeff King <peff@peff.net>]

On Fri, Mar 23, 2012 at 10:47:48AM -0700, Junio C Hamano wrote:

> Thomas Rast <trast@student.ethz.ch> writes:
> 
> > How about trying to read "HEAD" as "head" instead when core.ignorecase
> > is true?  That would allow us to catch such misconfiguration (which I
> > imagine can also happen accidentally if you mv a repository across FS
> > boundaries) and tell the user about it.
> 
> Do you mean something like this?
> 
> I do not like it.  It essentially amounts to checking with the FS every
> time we run Git.

I think Thomas's suggestion is to piggy-back it onto an existing file
lookup ("head" instead of "HEAD"), so you aren't doing any extra work.
However, I'm not sure that would be sufficient. If I copy a repo from a
case-insensitive filesystem to a case-sensitive one, what will the case
of "HEAD" be on the new filesystem?

If the original filesystem was case-preserving, I would expect "HEAD".
But on a true caseless filesystem, it could be either. Of course,
current git would already blow up if the file was copied as "head",
which makes me think this is probably a rare case. So maybe that is not
worth worrying about.

I dunno. I think Thomas's idea is clever, but is this actually a problem
in practice? The current discussion seems more like a documentation bug,
and I don't remember seeing anybody reporting issues moving a repo
across filesystems (presumably most people use clone or push, which
handle this properly).

-Peff