tuned signature;
authorwenzelm
Thu, 28 Mar 2024 11:45:45 +0100
changeset 80050 7d8a24c5559d
parent 80049 b525f783b784
child 80051 9cdc4f533b91
tuned signature;
src/Pure/Admin/component_bash_process.scala
src/Pure/System/components.scala
--- a/src/Pure/Admin/component_bash_process.scala	Thu Mar 28 11:35:39 2024 +0100
+++ b/src/Pure/Admin/component_bash_process.scala	Thu Mar 28 11:45:45 2024 +0100
@@ -22,9 +22,9 @@
     val component_date = Date.Format.alt_date(Date.now())
     val component_name = "bash_process-" + component_date
     val component_dir =
-      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
-
-    component_dir.write_platforms()
+      Components.Directory(target_dir + Path.basic(component_name))
+        .create(progress = progress)
+        .write_platforms()
 
 
     /* platform */
--- 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