src/Pure/Tools/task_statistics.scala
Thu, 07 Mar 2013 18:14:30 +0100 wenzelm avoid -Infinity which confuses JFreeChart histogram;
Fri, 22 Feb 2013 14:39:12 +0100 wenzelm updated headers;
Sun, 20 Jan 2013 13:55:15 +0100 wenzelm accomodate scala-2.9.2;
less more (0) -3 tip