author | wenzelm |
Wed, 12 Jun 2024 16:58:55 +0200 | |
changeset 80358 | 45b434464cd8 |
parent 80357 | fe123d033e76 |
child 80359 | bb4e95d19ecb |
--- a/src/Pure/General/bytes.scala Tue Jun 11 21:32:26 2024 +0200 +++ b/src/Pure/General/bytes.scala Wed Jun 12 16:58:55 2024 +0200 @@ -157,7 +157,8 @@ /* content */ - lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes) + lazy val sha1_digest: SHA1.Digest = + SHA1.make_digest { sha => sha.update(bytes, offset, length) } def is_empty: Boolean = length == 0