Subject: Re: bug#37907: --no-ignore-case option

From: Karl Berry <[email-masked]>
Date: Thu, 24 Oct 2019 15:27:58 -0600

See the attached patch.  Less than 10 minutes' work. :-)

Thanks Arnold!

    Grep guys - I'm pretty sure I've signed papwerwork for grep. 

copyright.list confirms that you have :).

    I chose '-g' since that letter was unused. It has no mnemonic value.

If a one-letter option is going to be used (I thought that might be too
intrusive), I suggest -j, as being next to -i. It's also unused.

Thanks again,
Karl