proper limit for read operation (amending ac4d53bc8f6b);
authorwenzelm
Tue, 02 Jul 2024 16:15:50 +0200
changeset 80473 09afc244bb5e
parent 80472 8f839104d460
child 80474 66ebeae3acdc
proper limit for read operation (amending ac4d53bc8f6b);
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)