src/Pure/System/components.scala

--- a/src/Pure/System/components.scala	Tue Mar 26 20:23:13 2024 +0100
+++ b/src/Pure/System/components.scala	Tue Mar 26 20:39:06 2024 +0100
@@ -202,9 +202,11 @@
     def README: Path = path + Path.basic("README")
     def LICENSE: Path = path + Path.basic("LICENSE")
 
-    def create(progress: Progress = new Progress): Directory = {
-      progress.echo("Creating component directory " + toString)
-      ssh.new_directory(path)
+    def create(progress: Progress = new Progress, permissive: Boolean = false): Directory = {
+      if (!permissive || !ssh.is_dir(path)) {
+        progress.echo("Creating component directory " + toString)
+        ssh.new_directory(path)
+      }
       ssh.make_directory(etc)
       this
     }