> "read0.l" and "readf.l" give different output when the input is from a
> console. That is, "echo ab|./read0.l" and "echo ab|./readf.l" give the
> same result, but starting the script and typing "ab", return and
> Ctrl+D give different results. *Dbg is off.
The reason is with how standard input is read, i.e. 'stdinByte_A' in
"src64/io.l", or 'stdinByte' in "src/io.c".
You see that there are explicit checks with isatty(STDIN_FILENO), and
bye(0) is called immediately when the console is interactive (i.e. when
standard input is connected to a terminal).
The reason is that for interactive usage it is surprising when the
process doesn't terminate in some cases upon Ctrl-D. IIRC this is due to
how the interpreter reads expressions from the input stream, involving a