# HG changeset patch
# User wenzelm
# Date 1121419582 -7200
# Node ID fade1d3a299527ad4a0ab9a97a226ffd0166ff02
# Parent  6389511d46097aa902347f6191c1b168909f3189
tuned;

diff -r 6389511d4609 -r fade1d3a2995 Admin/profiling_report
--- a/Admin/profiling_report	Thu Jul 14 20:32:37 2005 +0200
+++ b/Admin/profiling_report	Fri Jul 15 11:26:22 2005 +0200
@@ -27,7 +27,7 @@
 }
 
 foreach my $fun (keys %log) {
-    push @output, (sprintf "%8d %s\n", $log{$fun}, $fun);
+    push @output, (sprintf "%12d %s\n", $log{$fun}, $fun);
 }
 
 print (sort @output);