src/Pure/System/components.scala
changeset 80048 a213dd3c0b29
parent 80011 b082476a8036
child 80050 7d8a24c5559d
--- a/src/Pure/System/components.scala	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/Pure/System/components.scala	Thu Mar 28 11:29:25 2024 +0100
@@ -211,6 +211,10 @@
       this
     }
 
+    def write_platforms(
+      lines: List[String] = Platform.Family.list.map(family => family.toString + " = ")
+    ): Unit = File.write(platform_props, terminate_lines(lines))
+
     def get_platforms(): Platforms = {
       val props_path = platform_props.expand
       val props =