more operations;
authorwenzelm
Tue, 24 Jan 2023 17:25:00 +0100
changeset 77076 4471dbb3b7a0
parent 77075 973de7855948
child 77077 c2e8ba15a10a
more operations;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Jan 24 17:16:00 2023 +0100
+++ b/src/Pure/General/ssh.scala	Tue Jan 24 17:25:00 2023 +0100
@@ -209,6 +209,11 @@
     /* remote file-system */
 
     override def expand_path(path: Path): Path = path.expand_env(settings)
+    override def absolute_path(path: Path): Path = {
+      val path1 = expand_path(path)
+      if (path1.is_absolute) path1 else Path.explode(user_home) + path1
+    }
+
     def remote_path(path: Path): String = expand_path(path).implode
 
     override def bash_path(path: Path): String = Bash.string(remote_path(path))
@@ -355,6 +360,7 @@
     def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
 
     def expand_path(path: Path): Path = path.expand
+    def absolute_path(path: Path): Path = path.absolute
     def bash_path(path: Path): String = File.bash_path(path)
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file