Re: [NTG-pdftex] unbuffered vs. buffered terminal output