Tue, 14 May 2013 20:46:09 +0200 | wenzelm | more uniform Markup.print_real; | file | diff | annotate |
Fri, 15 Mar 2013 13:46:37 +0100 | wenzelm | simplified time_CPU and time_GC; | file | diff | annotate |
Sat, 05 Jan 2013 17:24:27 +0100 | wenzelm | more direct property names; | file | diff | annotate |
Mon, 31 Dec 2012 16:56:54 +0100 | wenzelm | include user counters as well; | file | diff | annotate |
Thu, 29 Nov 2012 10:45:25 +0100 | wenzelm | more uniform ML statistics; | file | diff | annotate |
Wed, 28 Nov 2012 17:18:53 +0100 | wenzelm | some support for ML runtime statistics; | file | diff | annotate |