changeset 75382 | 81673c441ce3 |
parent 75310 | 42baf7ffa088 |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/Thy/sessions.scala Thu Mar 31 22:24:11 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Mar 31 22:40:34 2022 +0200 @@ -1150,11 +1150,12 @@ val buf = ByteBuffer.allocate(n) var i = 0 var m = 0 - do { + var cont = true + while (cont) { m = file.read(buf) if (m != -1) i += m + cont = (m != -1 && n > i) } - while (m != -1 && n > i) if (i == n) { val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)