src/Pure/Thy/export.scala
changeset 76363 f7174238b5e3
parent 76351 2cee31cd92f0
child 76656 a8f452f7c503
--- a/src/Pure/Thy/export.scala	Sat Oct 22 19:51:08 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Oct 22 20:06:55 2022 +0200
@@ -224,8 +224,9 @@
             (results, true)
           })
 
-    def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
+    def make_entry(session_name: String, args0: Protocol.Export.Args, body: Bytes): Unit = {
       if (!progress.stopped && !body.is_empty) {
+        val args = if (db.is_server) args0.copy(compress = false) else args0
         consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
       }
     }