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 =