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 |