27 Jun
2014
27 Jun
'14
5:53 p.m.
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