# HG changeset patch
# User wenzelm
# Date 1739542980 -3600
# Node ID 843c2205b0768909917aa397c1f2eb463101f9bf
# Parent  15b5cd4c8f64c3d0ff5dae3326d86d36a916a253
proper treatment of empty content, which is never compressed;

diff -r 15b5cd4c8f64 -r 843c2205b076 src/Pure/General/file_store.scala
--- a/src/Pure/General/file_store.scala	Thu Feb 13 23:38:28 2025 +0100
+++ b/src/Pure/General/file_store.scala	Fri Feb 14 15:23:00 2025 +0100
@@ -92,7 +92,7 @@
     compressed: Boolean,
     body: Bytes
   ) {
-    require(name.nonEmpty && size >= 0 && (size > 0 || compressed))
+    require(name.nonEmpty && size >= 0 && (size > 0 || !compressed))
 
     def content(compress_cache: Compress.Cache = Compress.Cache.none): Bytes =
       if (compressed) body.uncompress(cache = compress_cache) else body