Re: Bug: git pull output and case sensitivity.

From: Jeff King <peff@peff.net>
Date: Mar 20, 2023, 17:16 UTC
Message-ID: <20230320171602.GB2615782@coredump.intra.peff.net>
In-Reply-To: <20230319062239.w37x64knfhfapbsn@tb-raspi4>

On Sun, Mar 19, 2023 at 07:22:40AM +0100, Torsten Bögershausen wrote:

Show 17 quoted lines

> On Sat, Mar 18, 2023 at 07:21:10PM +0000, dooagain wrote:
> > Thank you for filling out a Git bug report!
> > Please answer the following questions to help us understand your issue.
> >
> > What did you do before the bug happened? (Steps to reproduce your issue)
> >
> > I configured my git repository to ignore case by executing `git config core.ignorecase true` then I executed `git pull` multiple times.
> 
> What do you mean by "I configured my git repository" ?
> The answer is already there, so let's re-rephrase it:
> Are you working on a case-insensitive file system ?
> 
> What happens if you create a test directory, like this:
> mkdir test-case
> cd test-case
> git init
> git config --get  core.ignorecase

I think this is kind of a red herring, isn't it? The bug report is about refs, and I don't think those really respect core.ignorecase either way, and inconsistencies are known to happen on case-insensitive filesystems (because the refs are sometimes case-sensitive and sometimes not depending on whether they are packed or loose in the filesystem).

So I think this is just a known gotcha, and the path forward is probably a new ref storage format that doesn't rely on storing names directly in the filesystem (reftable, or some system based on packed-ref slices).

-Peff