# HG changeset patch
# User wenzelm
# Date 1689507946 -7200
# Node ID fca9ec5a615c6aaba3c87289b9e067adab05cab0
# Parent  8da30ae02dda92d39af1f09fabccab5782aac3a8
tuned output;

diff -r 8da30ae02dda -r fca9ec5a615c src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 13:41:00 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 13:45:46 2023 +0200
@@ -477,7 +477,7 @@
       def trace(msg: String, nl: Boolean = false): Unit = {
         val trace_time = Time.now() - trace_start
         if (trace_time >= trace_min) {
-          val nl = if (trace_nl) { trace_nl = true; "\n" } else ""
+          val nl = if (trace_nl) "" else { trace_nl = true; "\n" }
           log(nl + trace_time + " transaction " + trace_count +
             if_proper(label, " " + label) + ": " + msg)
         }