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)
       }
     }