--- a/src/Pure/Admin/component_bash_process.scala Thu Mar 28 08:30:42 2024 +0100
+++ b/src/Pure/Admin/component_bash_process.scala Thu Mar 28 11:29:25 2024 +0100
@@ -24,6 +24,8 @@
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
+ component_dir.write_platforms()
+
/* platform */
@@ -179,12 +181,6 @@
""")
- /* platform.props */
-
- File.write(component_dir.platform_props,
- Platform.Family.list.map(family => family.toString + " = ").mkString("", "\n", "\n"))
-
-
/* README */
File.write(component_dir.README,
--- 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 =