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 }