On Thu, Oct 12, 2017 at 11:34 PM, Bernhard Voelker
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 th
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
* doc/grep.texi (Other options): Do the above.
Reported in
https://lists.opensuse.org/opensuse/2017-03/msg00411.html
---
doc/grep.texi | 8
1 file changed, 8 insertions(+)
diff --git a/doc/grep.texi b/doc/grep.texi
index 077c05f..2bc3435 100644
--- a/doc/grep.texi
+++ b/doc/grep.texi
@@
