| changeset 73385 | 1892708fd148 |
| parent 73340 | 0ffcad1f6130 |
| child 73702 | 7202e12cb324 |
--- 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])