# HG changeset patch
# User wenzelm
# Date 1689602999 -7200
# Node ID 9c86b609eeb6d8d85879ae01f1ef91ff67cde1a0
# Parent  f8e3b228670cbd802db0c39b2e7f9e1b07b05cad
removed junk (amending f8e3b228670c);

diff -r f8e3b228670c -r 9c86b609eeb6 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Jul 17 16:02:28 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Jul 17 16:09:59 2023 +0200
@@ -474,7 +474,7 @@
 
       def trace(msg: String): Unit = {
         val trace_time = Time.now() - trace_start
-        if (trace_time >= trace_minx) {
+        if (trace_time >= trace_min) {
           val nl = if (trace_nl) "" else { trace_nl = true; "\n" }
           log(nl + trace_time + " transaction " + trace_count +
             if_proper(label, " " + label) + ": " + msg)