diff -r 2a0051496844 -r 985c3a64748c src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Fri Aug 05 13:34:47 2022 +0200 +++ b/src/Pure/Thy/export.scala Fri Aug 05 13:43:14 2022 +0200 @@ -239,9 +239,9 @@ (results, true) }) - def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = { - if (!progress.stopped) { - consumer.send(make_entry(session_name, args, body, cache) -> args.strict) + def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = { + if (!progress.stopped && !body.is_empty) { + consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict) } }