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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
