author | wenzelm |
Fri, 05 Mar 2021 16:45:16 +0100 | |
changeset 73385 | 1892708fd148 |
parent 73384 | d21dbfd3d69b |
child 73386 | 3fb201ca8fb5 |
--- a/src/Pure/General/time.scala Fri Mar 05 16:44:04 2021 +0100 +++ b/src/Pure/General/time.scala Fri Mar 05 16:45:16 2021 +0100 @@ -21,7 +21,6 @@ def now(): Time = ms(System.currentTimeMillis()) val zero: Time = ms(0) - val start: Time = now() def print_seconds(s: Double): String = String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])