# HG changeset patch # User wenzelm # Date 1718204335 -7200 # Node ID 45b434464cd83fc1921b55dc8f5fcc65b50e4769 # Parent fe123d033e76e2c6c3a9de0be17220a74e03ce65 proper sha1_digest: need to include offset + length; diff -r fe123d033e76 -r 45b434464cd8 src/Pure/General/bytes.scala --- 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