bug#41700: grep -v always exiting with 1 for empty file

[Paul Eggert]

On 6/4/20 1:34 PM, Eric Blake wrote:
>>> in your definition would
>>>
>>> echo -n foo > file
>>>
>>> (so no newline, but non zero length)
>>
>> No, the file has zero length:
>>
>> $ echo -n >file
> 
> You missed the 'echo -n foo' that prints 3 bytes to file.

Ah sorry, indeed I did. In that case my interpretation indeed agrees with yours.