diff -r 807a5d219c23 -r 46acd255810d src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Fri Mar 02 21:45:45 2012 +0100
+++ b/src/Pure/General/time.scala	Sat Mar 03 11:09:17 2012 +0100
@@ -21,8 +21,11 @@
   def min(t: Time): Time = if (ms < t.ms) this else t
   def max(t: Time): Time = if (ms > t.ms) this else t
 
+  def is_relevant: Boolean = ms >= 1
+
   override def toString =
     String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+
   def message: String = toString + "s"
 }