removed unused/pointless operation: Time.start is the load/init time of this Scala module;
authorwenzelm
Fri, 05 Mar 2021 16:45:16 +0100
changeset 73385 1892708fd148
parent 73384 d21dbfd3d69b
child 73386 3fb201ca8fb5
removed unused/pointless operation: Time.start is the load/init time of this Scala module;
src/Pure/General/time.scala
--- 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])