# HG changeset patch
# User wenzelm
# Date 1647977152 -3600
# Node ID dc1c53d14c3829976abfe55b91d731d3f3f301cb
# Parent  e8c1d982b2752f8c8e119ded42e5302291139fbc
tuned -- follow sha1_digest in src/Tools/Setup/src/Build.java;

diff -r e8c1d982b275 -r dc1c53d14c38 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Tue Mar 22 20:06:41 2022 +0100
+++ b/src/Pure/General/sha1.scala	Tue Mar 22 20:25:52 2022 +0100
@@ -9,6 +9,8 @@
 
 import java.io.{File => JFile, FileInputStream}
 import java.security.MessageDigest
+import java.util.Locale
+import java.math.BigInteger
 
 
 object SHA1
@@ -24,16 +26,8 @@
     override def toString: String = rep
   }
 
-  private def make_result(digest: MessageDigest): Digest =
-  {
-    val result = new StringBuilder
-    for (b <- digest.digest()) {
-      val i = b.asInstanceOf[Int] & 0xFF
-      if (i < 16) result += '0'
-      result ++= Integer.toHexString(i)
-    }
-    new Digest(result.toString)
-  }
+  private def sha1_digest(sha: MessageDigest): Digest =
+    new Digest(String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())))
 
   def fake(rep: String): Digest = new Digest(rep)
 
@@ -51,7 +45,7 @@
       } while (m != -1)
     })
 
-    make_result(digest)
+    sha1_digest(digest)
   }
 
   def digest(path: Path): Digest = digest(path.file)
@@ -61,7 +55,7 @@
     val digest = MessageDigest.getInstance("SHA")
     digest.update(bytes)
 
-    make_result(digest)
+    sha1_digest(digest)
   }
 
   def digest(bytes: Bytes): Digest = bytes.sha1_digest