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



Reply via email to