On 27/06/2014 12:03, Makarius wrote:
What are the conditions under which Poly/ML 5.5.2 creates a directory
$HOME/.polyml and puts poly-stats files there?
Poly/ML always creates a .polyml directory and a poly-stats file. The
poly-stats file will be deleted when the Poly/ML process finishes
normally. If it crashes, though, the file will remain.
I am also using PolyML.Statistics.getLocalStats, but shouldn't the
shared-memory file be for global stats only?
The Poly/ML process does not know when another process wants to read the
statistics so they are always made available as a memory-mapped file.
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
