# HG changeset patch
# User nipkow
# Date 1251984605 -7200
# Node ID 212530b16e6eebd494f5a7f6f8c19414ce352e0e
# Parent  52b4f2f54e466e7513bf38569284905271ebc1a8
scaled avg_time

diff -r 52b4f2f54e46 -r 212530b16e6e src/HOL/Mirabelle/lib/scripts/report.pl
--- a/src/HOL/Mirabelle/lib/scripts/report.pl	Thu Sep 03 14:50:02 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/report.pl	Thu Sep 03 15:30:05 2009 +0200
@@ -55,7 +55,7 @@
 if ($sh_calls > 0) {
   my $percent = $sh_succeeded / $sh_calls * 100;
   my $time = $sh_time / 1000;
-  my $avg_time = $sh_time / $sh_succeeded;
+  my $avg_time = $time / $sh_succeeded;
   print FILE "Total number of sledgehammer calls: $sh_calls\n";
   print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
   printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;