tuned signature;
authorwenzelm
Wed, 12 Feb 2025 20:18:21 +0100
changeset 82150 2eb2aa0375fb
parent 82149 18709ffb8137
child 82151 a42414afe05f
tuned signature;
src/Pure/General/file_store.scala
--- a/src/Pure/General/file_store.scala	Wed Feb 12 20:05:42 2025 +0100
+++ b/src/Pure/General/file_store.scala	Wed Feb 12 20:18:21 2025 +0100
@@ -77,12 +77,12 @@
   ) {
     require(name.nonEmpty && size >= 0 && (size > 0 || compressed))
 
-    def content(cache: Compress.Cache = Compress.Cache.none): Bytes =
-      if (compressed) body.uncompress(cache = cache) else body
+    def content(compress_cache: Compress.Cache = Compress.Cache.none): Bytes =
+      if (compressed) body.uncompress(cache = compress_cache) else body
 
-    def write_file(dir: Path, cache: Compress.Cache = Compress.Cache.none): Unit = {
+    def write_file(dir: Path, compress_cache: Compress.Cache = Compress.Cache.none): Unit = {
       val path = Path.explode(name)
-      File.content(path, content(cache = cache)).write(dir)
+      File.content(path, content(compress_cache = compress_cache)).write(dir)
       if (executable) File.set_executable(dir + path)
     }
   }