src/Pure/Admin/component_polyml.scala
changeset 81927 d59262da07ac
parent 80224 db92e0b6a11a
child 82142 508a673c87ac
--- a/src/Pure/Admin/component_polyml.scala	Sun Jan 19 15:13:42 2025 +0100
+++ b/src/Pure/Admin/component_polyml.scala	Sun Jan 19 15:36:12 2025 +0100
@@ -195,8 +195,8 @@
     /* component */
 
     val component_name1 = if (component_name.isEmpty) "polyml-" + polyml_version else component_name
-    val component_dir = Components.Directory(target_dir + Path.basic(component_name1)).create()
-    progress.echo("Component " + component_dir)
+    val component_dir =
+      Components.Directory(target_dir + Path.basic(component_name1)).create(progress = progress)
 
 
     /* download and build */