--- 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)