Makarius wrote:
On Thu, 13 May 2010, David Matthews wrote:
I guess an alternative would be to use
an extra internal (blocking) thread and pipe and have the ML thread
use "select" on the pipe.
This sounds like a considerable complication to address such a minor
issue.
Well, there's code in the Windows-specific part to do this for pipes in
Windows which suffer a similar problem. It's probably more important in
that situation because it affects each read from a pipe not just the
detection of when the process has completed. I don't think it would be
hard to do the same for process termination in Unix.
Are 10ms adequate for the Wait above? Can anything bad happen here?
I can't see any reason why there should be a problem. Essentially, it's
a matter of avoiding wasting too many CPU cycles with unnecessary
polling. I could make the same change in Poly/ML SVN.
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
