changeset 57912 | dd9550f84106 |
parent 56691 | ad5d7461b370 |
child 61528 | 053f7083b3eb |
--- a/src/Pure/General/time.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/General/time.scala Tue Aug 12 15:46:20 2014 +0200 @@ -40,7 +40,7 @@ def is_zero: Boolean = ms == 0 def is_relevant: Boolean = ms >= 1 - override def toString = Time.print_seconds(seconds) + override def toString: String = Time.print_seconds(seconds) def message: String = toString + "s" }