# HG changeset patch
# User wenzelm
# Date 1605731995 -3600
# Node ID 99a6bcd1e8e4bd907891b952c6854e437ab1a517
# Parent  ea35afdb13668d8bc95dc363b6001b56350c865c
tuned signature;

diff -r ea35afdb1366 -r 99a6bcd1e8e4 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Wed Nov 18 21:34:13 2020 +0100
+++ b/src/Pure/General/sha1.scala	Wed Nov 18 21:39:55 2020 +0100
@@ -66,6 +66,8 @@
 
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
   def digest(string: String): Digest = digest(Bytes(string))
+  def digest_set(digests: List[Digest]): Digest =
+    digest(cat_lines(digests.map(_.toString).sorted))
 
   val digest_length: Int = digest("").rep.length
 }
diff -r ea35afdb1366 -r 99a6bcd1e8e4 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 18 21:34:13 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 18 21:39:55 2020 +0100
@@ -440,7 +440,7 @@
 
           val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
           val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
-          val sources = SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
+          val sources = SHA1.digest_set(digests).toString
           prepare_dir2(tmp_dir, doc)
 
           doc_output.foreach(prepare_dir1(_, doc))
diff -r ea35afdb1366 -r 99a6bcd1e8e4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 18 21:34:13 2020 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 18 21:39:55 2020 +0100
@@ -533,7 +533,7 @@
         full_sessions(session_name).meta_digest ::
         deps.sources(session_name) :::
         deps.imported_sources(session_name)
-      SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
+      SHA1.digest_set(digests).toString
     }
 
     val deps =