Subject: Re: GREP_OPTIONS not processed

From: Paul Eggert <[email-masked]>
Date: Tue, 31 Dec 2019 12:02:34 -0800

No further comment on this bug report for two years, and I still cannot
reproduce it. Closing the bug report.