diff -r b75fefe1ddb5 -r 583ad7a9941c src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Fri Mar 25 16:41:03 2022 +0100
+++ b/src/Pure/General/sha1.scala	Fri Mar 25 17:00:12 2022 +0100
@@ -24,6 +24,7 @@
         case other: Digest => rep == other.toString
         case _ => false
       }
+    def shasum(name: String): String = rep + " " + name
   }
 
   def fake_digest(rep: String): Digest = new Digest(rep)