src/Pure/General/timing.scala
changeset 57912 dd9550f84106
parent 56782 433cf57550fa
child 62571 2fd90993a928
--- a/src/Pure/General/timing.scala	Tue Aug 12 15:31:24 2014 +0200
+++ b/src/Pure/General/timing.scala	Tue Aug 12 15:46:20 2014 +0200
@@ -38,6 +38,6 @@
   def message: String =
     elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
 
-  override def toString = message
+  override def toString: String = message
 }