On Thu, Oct 12, 2017 at 11:34 PM, Bernhard Voelker <m...@bernhard-voelker.de> wrote: > On 03/17/2017 11:42 AM, Bernhard Voelker wrote: >> [...] > > ping? I don't have permissions to push at 'grep.git', so someone > else needs to do this, thanks.
Thanks, Bernie. I've pushed that, after adjusting the commit log to mention the bug URL, http://bugs.gnu.org/26139
