src/Pure/General/file.scala
changeset 77852 df35b5b7b6a4
parent 77218 86217697863c
child 78158 8b5a2e4b16d4
--- a/src/Pure/General/file.scala	Fri Apr 14 22:19:28 2023 +0200
+++ b/src/Pure/General/file.scala	Fri Apr 14 22:55:01 2023 +0200
@@ -383,10 +383,10 @@
   final class Content private[File](val path: Path, val content: Bytes) {
     override def toString: String = path.toString
 
-    def write(dir: Path): Unit = {
+    def write(dir: Path, ssh: SSH.System = SSH.Local): Unit = {
       val full_path = dir + path
-      Isabelle_System.make_directory(full_path.expand.dir)
-      Bytes.write(full_path, content)
+      ssh.make_directory(ssh.expand_path(full_path).dir)
+      ssh.write_bytes(full_path, content)
     }
   }