# HG changeset patch
# User wenzelm
# Date 1678311615 -3600
# Node ID 832139c1b268ee8b4b806b255595982058727a25
# Parent  3f3dcf9f53f1a87aeaaea96775407da905565c6f
proper shasum lines (amending 3070001c9d1f);

diff -r 3f3dcf9f53f1 -r 832139c1b268 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 **/