changeset 71775 | 291c46bf3000 |
parent 69393 | ed0824ef337e |
child 72654 | 99a6bcd1e8e4 |
--- a/src/Pure/General/sha1.scala Tue Apr 21 19:07:11 2020 +0200 +++ b/src/Pure/General/sha1.scala Tue Apr 21 19:07:49 2020 +0200 @@ -45,12 +45,10 @@ { val buf = new Array[Byte](65536) var m = 0 - try { - do { - m = stream.read(buf, 0, buf.length) - if (m != -1) digest.update(buf, 0, m) - } while (m != -1) - } + do { + m = stream.read(buf, 0, buf.length) + if (m != -1) digest.update(buf, 0, m) + } while (m != -1) }) make_result(digest)