changeset 80050 | 7d8a24c5559d |
parent 80048 | a213dd3c0b29 |
child 80219 | 840ca997deac |
--- a/src/Pure/System/components.scala Thu Mar 28 11:35:39 2024 +0100 +++ b/src/Pure/System/components.scala Thu Mar 28 11:45:45 2024 +0100 @@ -213,7 +213,10 @@ def write_platforms( lines: List[String] = Platform.Family.list.map(family => family.toString + " = ") - ): Unit = File.write(platform_props, terminate_lines(lines)) + ): Directory = { + File.write(platform_props, terminate_lines(lines)) + this + } def get_platforms(): Platforms = { val props_path = platform_props.expand