| changeset 80360 | 6ea999f55c2d |
| parent 80359 | bb4e95d19ecb |
| child 80361 | 54a83e8e447b |
--- a/src/Pure/General/bytes.scala Wed Jun 12 21:40:13 2024 +0200 +++ b/src/Pure/General/bytes.scala Wed Jun 12 21:44:30 2024 +0200 @@ -158,8 +158,7 @@ /* content */ lazy val sha1_digest: SHA1.Digest = - if (is_empty) SHA1.digest_empty - else SHA1.make_digest { sha => sha.update(bytes, offset, length) } + if (is_empty) SHA1.digest_empty else SHA1.digest(bytes, offset, length) def is_empty: Boolean = length == 0