# HG changeset patch
# User wenzelm
# Date 1718221470 -7200
# Node ID 6ea999f55c2d5076a146670a5534fa715e279621
# Parent  bb4e95d19ecb09c3a2dc832cd619ba76b808754c
tuned signature;

diff -r bb4e95d19ecb -r 6ea999f55c2d src/Pure/General/bytes.scala
--- 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
 
diff -r bb4e95d19ecb -r 6ea999f55c2d src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Wed Jun 12 21:40:13 2024 +0200
+++ b/src/Pure/General/sha1.scala	Wed Jun 12 21:44:30 2024 +0200
@@ -49,6 +49,8 @@
 
   def digest(path: Path): Digest = digest(path.file)
   def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes))
+  def digest(bytes: Array[Byte], offset: Int, length: Int): Digest =
+    make_digest(_.update(bytes, offset, length))
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
   def digest(string: String): Digest = digest(Bytes(string))