| changeset 53292 | f567c1c7b180 |
| parent 51587 | 7050c4656fd8 |
| child 56351 | 1c735e46acf0 |
--- a/src/Pure/General/time.scala Thu Aug 29 20:46:55 2013 +0200 +++ b/src/Pure/General/time.scala Thu Aug 29 21:17:46 2013 +0200 @@ -30,6 +30,7 @@ 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_zero: Boolean = ms == 0 def is_relevant: Boolean = ms >= 1 override def hashCode: Int = ms.hashCode