# HG changeset patch
# User wenzelm
# Date 1614959116 -3600
# Node ID 1892708fd14864665202793339297aa2dd26c7da
# Parent  d21dbfd3d69b6b34f7869324040bbc820076f0a0
removed unused/pointless operation: Time.start is the load/init time of this Scala module;

diff -r d21dbfd3d69b -r 1892708fd148 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])