On Fri, Jan 17, 2025 at 6:25 PM David G. Johnston <david(dot)g(dot)johnston(at)gmail(dot)com> wrote:
> Otherwise, those should be output on stdout;>
That should say "stderr".
David J.