author | wenzelm |
Wed, 08 Mar 2023 22:40:15 +0100 | |
changeset 77592 | 832139c1b268 |
parent 77591 | 3f3dcf9f53f1 |
child 77593 | 08ed864fed24 |
--- 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 **/