diff -r 1928405a409b -r f7174238b5e3 src/Pure/Thy/export.scala --- 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) } }