Re: makeinfo should accept /dev/fd/0 argument

[Karl Berry]

    'makeinfo' refuses to read from stdin when it is named /dev/fd/0
 
Thanks for the report.