# HG changeset patch
# User wenzelm
# Date 1718284104 -7200
# Node ID d5c48fe601b63303821068be440259db9810f74a
# Parent  306f273c91ec6917f7d5f51a9fd895ecfb54402e
tuned;

diff -r 306f273c91ec -r d5c48fe601b6 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jun 12 22:09:16 2024 +0200
+++ b/src/Pure/General/bytes.scala	Thu Jun 13 15:08:24 2024 +0200
@@ -76,14 +76,14 @@
     if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)
     else if (len == 0L) empty
     else {
-      using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { java_path =>
-        java_path.position(start)
+      using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { channel =>
+        channel.position(start)
         val n = len.toInt
         val buf = ByteBuffer.allocate(n)
         var i = 0
         var m = 0
         while ({
-          m = java_path.read(buf)
+          m = channel.read(buf)
           if (m != -1) i += m
           m != -1 && n > i
         }) ()