Subject: Re: bug#38792: man grep

From: Paul Eggert <[email-masked]>
Date: Mon, 21 Sep 2020 12:09:56 -0700

Discussion on this worthsmithing issue died down in December so I'm taking the 
liberty of closing the bug report. We can reopen it or start a new one as necessary.