27 Jun
2014
27 Jun
'14
12:03 p.m.
Just a quick question, before I study the Poly/ML sources in detail.
What are the conditions under which Poly/ML 5.5.2 creates a directory $HOME/.polyml and puts poly-stats files there?
I have recently found by accident that I have hundreds of such files lying around. Maybe I just got some Poly/ML build/run options wrong, such that statistics are enabled accidentally.
I am also using PolyML.Statistics.getLocalStats, but shouldn't the shared-memory file be for global stats only?
Makarius