| changeset 63688 | cc57255bf6ae |
| parent 63686 | 66f217416da7 |
| child 63700 | 2a95d904672e |
--- a/src/Pure/General/time.scala Sat Aug 13 23:33:58 2016 +0200 +++ b/src/Pure/General/time.scala Sat Aug 13 23:45:29 2016 +0200 @@ -29,6 +29,7 @@ final class Time private(val ms: Long) extends AnyVal { def seconds: Double = ms / 1000.0 + def minutes: Double = ms / 60000.0 def + (t: Time): Time = new Time(ms + t.ms) def - (t: Time): Time = new Time(ms - t.ms)