diff -r 18709ffb8137 -r 2eb2aa0375fb 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) } }