| changeset 61602 | a2f0f659a3c2 |
| parent 61528 | 053f7083b3eb |
| child 62571 | 2fd90993a928 |
--- a/src/Pure/General/time.scala Sat Nov 07 20:04:09 2015 +0100 +++ b/src/Pure/General/time.scala Sun Nov 08 14:41:07 2015 +0100 @@ -31,6 +31,7 @@ def + (t: Time): Time = new Time(ms + t.ms) def - (t: Time): Time = new Time(ms - t.ms) + def compare(t: Time): Int = ms compare t.ms def < (t: Time): Boolean = ms < t.ms def <= (t: Time): Boolean = ms <= t.ms def > (t: Time): Boolean = ms > t.ms