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

From: Stefan Kangas <[email-masked]>
Date: Wed, 6 Jul 2022 12:40:05 +0200

Phil Sainty <[email-masked]> writes:

> I agree that "fold" isn't intuitive to newcomers, but I also think
> it's good to try to limit the number of different terms used to
> express a concept.

Agreed, though I would add that it isn't intuitive to old users either
(case in point: me).  So let's start moving in the right direction.