| 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 |