| Sat, 06 Nov 2010 16:31:35 +0100 | wenzelm | explicit "timing" status for toplevel transactions; | file | diff | annotate |
| Thu, 04 Nov 2010 10:22:59 +0100 | wenzelm | tuned; | file | diff | annotate |
| Tue, 02 Nov 2010 20:31:46 +0100 | wenzelm | added convenience operation seconds: real -> time; | file | diff | annotate |
| Wed, 14 Oct 2009 23:13:38 +0200 | wenzelm | show direct GC time (which is included in CPU time); | file | diff | annotate |
| Mon, 22 Jun 2009 22:51:08 +0200 | wenzelm | end_timing: checked divisions with sane defaults; | file | diff | annotate |
| Wed, 17 Jun 2009 18:02:51 +0200 | wenzelm | end_timing: actually display GC percentage, not factor; | file | diff | annotate |
| Wed, 17 Jun 2009 17:06:07 +0200 | wenzelm | more detailed start_timing/end_timing (in timing.ML); | file | diff | annotate |