src/Pure/General/time.scala
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"
 }