Re: another serious `texi2dvi -E' bug

[Karl Berry]

    How is it known that output is not piped through? 

No -o -

    And also shouldn't @setfilename the_file (line read from STDIN) be
    honored if there is such line in the input?

Yes.  And makeinfo does so, as far as I could tell.  stdin.info is
created in cases like
  echo foo | makeinfo

    Right. I plan to modify --help to say:

At least when invoked as makeinfo, I think the help message should look
the way makeinfo --help does now.  A fair amount of work has gone into
that over the years.

Thanks,
Karl