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
