proper treatment of empty content, which is never compressed;
authorwenzelm
Fri, 14 Feb 2025 15:23:00 +0100
changeset 82161 843c2205b076
parent 82160 15b5cd4c8f64
child 82162 5ecd0209c0a8
proper treatment of empty content, which is never compressed;
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