# HG changeset patch
# User wenzelm
# Date 1719929750 -7200
# Node ID 09afc244bb5e1f7427795e31322b088813e9d01e
# Parent  8f839104d460e790337d4b48b6222be6cebbd40e
proper limit for read operation (amending ac4d53bc8f6b);

diff -r 8f839104d460 -r 09afc244bb5e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Tue Jul 02 15:30:59 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jul 02 16:15:50 2024 +0200
@@ -90,10 +90,13 @@
       Builder.use(hint = stop) { builder =>
         using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { channel =>
           channel.position(start)
+          val buf_size = block_size
           val buf = ByteBuffer.allocate(block_size)
           var m = 0
           var n = 0L
           while ({
+            val l = stop - n
+            if (l < buf_size) buf.limit(l.toInt)
             m = channel.read(buf)
             if (m != -1) {
               builder += (buf.array(), 0, m)