Subject: Re: bug#56401: "Case folding" should be called "ignore case"

From: Stefan Kangas <[email-masked]>
Date: Tue, 5 Jul 2022 19:11:00 +0200

Lars Ingebrigtsen <[email-masked]> writes:

> I agree that "ignore case" would be better, but it somehow seems like
> most people don't have much problem with the "case folding" terminology?

I had to look up the exact meaning today, FWIW.

(I confused myself on whether or not "case folding" is the same as
"ignore case" or its inverse.)