# HG changeset patch # User wenzelm # Date 1639593057 -3600 # Node ID afd8cb7b2be102b8d0b562cc2fb787556479077e # Parent 9ddf227fc8a43f8971bf41a07cac1067e07f43ce tuned imports; diff -r 9ddf227fc8a4 -r afd8cb7b2be1 src/Pure/General/date.scala --- a/src/Pure/General/date.scala Wed Dec 15 15:26:31 2021 +0100 +++ b/src/Pure/General/date.scala Wed Dec 15 19:30:57 2021 +0100 @@ -8,12 +8,11 @@ import java.util.Locale -import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime} +import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId} import java.time.format.{DateTimeFormatter, DateTimeParseException} import java.time.temporal.TemporalAccessor import scala.annotation.tailrec -import scala.math.Ordering object Date