author | wenzelm |
Sun, 16 Jul 2023 12:34:30 +0200 | |
changeset 78360 | 1f074427ad2b |
parent 78359 | cb0a90df4871 |
child 78361 | b625cdabf963 |
--- 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) {