# HG changeset patch
# User wenzelm
# Date 1689500612 -7200
# Node ID 0cecb723629838f0b69f1fef2f79b04ae114313e
# Parent  974dbe256a37564d16eb4ba48cf20bc37309d93a
more operations;

diff -r 974dbe256a37 -r 0cecb7236298 src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Sun Jul 16 11:29:23 2023 +0200
+++ b/src/Pure/General/time.scala	Sun Jul 16 11:43:32 2023 +0200
@@ -20,6 +20,8 @@
   def now(): Time = ms(System.currentTimeMillis())
 
   val zero: Time = ms(0)
+  val min: Time = ms(Long.MinValue)
+  val max: Time = ms(Long.MaxValue)
 
   def print_seconds(s: Double): String =
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])