# HG changeset patch # User wenzelm # Date 1689503670 -7200 # Node ID 1f074427ad2b62271e437cb0875993a4690eccf6 # Parent cb0a90df4871cb0d8fbfde3c1439255eb0a5c7f1 tuned output; diff -r cb0a90df4871 -r 1f074427ad2b src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sun Jul 16 12:19:48 2023 +0200 +++ b/src/Pure/Thy/export.scala Sun Jul 16 12:34:30 2023 +0200 @@ -238,7 +238,7 @@ consume = { (args: List[(Entry, Boolean)]) => val results = - Data.transaction_lock(db, label = "Export.consumer") { + Data.transaction_lock(db, label = "Export.consumer(" + args.length + ")") { for ((entry, strict) <- args) yield { if (progress.stopped) {