# HG changeset patch
# User wenzelm
# Date 1689509976 -7200
# Node ID bb5e2a7198e330591a301b83e69226b96f79b671
# Parent  e33cca11b474bd6d5c88ba4e3cc356c29d56df7b
more standard time unit;

diff -r e33cca11b474 -r bb5e2a7198e3 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 14:11:56 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 14:19:36 2023 +0200
@@ -464,7 +464,7 @@
       val prop = "isabelle.transaction_trace"
       val trace_min =
         System.getProperty(prop, "") match {
-          case Value.Long(ms) => Time.ms(ms)
+          case Value.Seconds(t) => t
           case "true" => Time.min
           case "false" | "" => Time.max
           case s => error("Bad system property " + prop + ": " + quote(s))