proper shasum lines (amending 3070001c9d1f);
authorwenzelm
Wed, 08 Mar 2023 22:40:15 +0100
changeset 77592 832139c1b268
parent 77591 3f3dcf9f53f1
child 77593 08ed864fed24
proper shasum lines (amending 3070001c9d1f);
src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Wed Mar 08 22:22:35 2023 +0100
+++ b/src/Pure/System/components.scala	Wed Mar 08 22:40:15 2023 +0100
@@ -230,7 +230,7 @@
       })
 
   def write_components_sha1(entries: List[SHA1_Entry]): Unit =
-    File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
+    File.write(components_sha1, entries.sortBy(_.name).mkString)
 
 
   /** manage user components **/