> I don't think this distinction is necessary, either you have a
> case-insensitive file system or you don't. The case
> that the .git directory is case-sensitive and the worktree directory isn't
> (or the other way around) is
> probably so exotic that we can ignore it.
I think Torsten's use case was for someone who is carefully curating
their loose and packed-refs, e.g. gc.packrefs = false. This could be
for backwards compatibility (existing ambiguous refs whose names
cannot be changed for some reason) or simply because they want to.
> If you want to prevent problems with Windows/Mac OS, you should set
> core.ignorecase = true. I don't see why we need
> yet another config setting for refs (and logs?).
Since refs.ignorecase falls back to core.ignorecase, you could just
set core.ignorecase = true and feel safe when sharing with Windows/Mac
OS. I think having the distinction just makes Git more flexible, OTOH
I can see how having both refs.ignorecase and core.ignorecase could be
confusing and possibly redundant.
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majord...@vger.kernel.org
More majordomo info at http://vger.kernel.org/majordomo-info.html