Hi Karl. See the attached patch. Less than 10 minutes' work. :-) Grep guys - I'm pretty sure I've signed papwerwork for grep. Feel free to incorporate this patch. I chose '-g' since that letter was unused. It has no mnemonic value. Thanks, Arnold Karl Berry wrote: > I suggest adding --no-ignore-case to clear the case-insensitivity -i > search. I, and surely many others, have an alias or script that runs > grep with -i by default, along with other options (since GREP_OPTIONS > was killed). It would be highly convenient to be able to add > --no-ignore-case on the fly to the rare-in-my-experience invocations > where case sensitivity is desired. > > (Also, just in principle, it seems like any boolean option should be > switchable by successive options. But I won't go that far.) > > Besides, since I'm not sending a patch (sorry), my expectation is that > there will never be enough time to implement random minor suggestions > like this, so it doesn't matter :). > > Thanks, > Karl