[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#26139: [PATCH] doc: document the option delimiter '--'
|
From: |
Jim Meyering |
|
Subject: |
bug#26139: [PATCH] doc: document the option delimiter '--' |
|
Date: |
Fri, 13 Oct 2017 08:47:40 -0700 |
On Thu, Oct 12, 2017 at 11:34 PM, Bernhard Voelker
<address@hidden> 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