bug#26139: [PATCH] doc: document the option delimiter '--'

[Bernhard Voelker]

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.

Have a nice day,
Berny