diff -r d4c89ea5e6dc -r acdfc76a6c33 NEWS --- a/NEWS Mon Dec 21 14:18:57 2015 +0100 +++ b/NEWS Mon Dec 21 15:09:35 2015 +0100 @@ -669,6 +669,13 @@ tools, but can also cause INCOMPATIBILITY for tools that don't observe the proof context discipline. +* The following combinators for low-level profiling of the ML runtime +system are available: + + profile_time (*CPU time*) + profile_time_thread (*CPU time on this thread*) + profile_allocations (*overall heap allocations*) + *** System ***