# HG changeset patch
# User wenzelm
# Date 1362676470 -3600
# Node ID 716a94cc5aaf1f4dbc11c11f26b2fca946020e80
# Parent  960b0ca9ae5dbfd6e8a3370174001a3cae403f61
avoid -Infinity which confuses JFreeChart histogram;

diff -r 960b0ca9ae5d -r 716a94cc5aaf src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Thu Mar 07 17:50:26 2013 +0100
+++ b/src/Pure/Tools/task_statistics.scala	Thu Mar 07 18:14:30 2013 +0100
@@ -32,8 +32,8 @@
   def chart(bins: Int = 100): JFreeChart =
   {
     val values = new Array[Double](tasks.length)
-    for ((Run(x), i) <- tasks.iterator.zipWithIndex) values(i) =
-      java.lang.Math.log10(x.toDouble / 1000000)
+    for ((Run(x), i) <- tasks.iterator.zipWithIndex)
+      values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000)
 
     val data = new HistogramDataset
     data.addSeries("tasks", values, bins)