>You could try using -outfile instead of redirection.

That did the trick.  Now does anyone know why -outfile minics output to
a terminal while redirection does not?  What's the difference between
them?

David

Reply via email to