# HG changeset patch
# User wenzelm
# Date 1674577500 -3600
# Node ID 4471dbb3b7a072eecd0be63be91c3d681963793c
# Parent  973de7855948c9e436ccf8e24c95ed61338e4b25
more operations;

diff -r 973de7855948 -r 4471dbb3b7a0 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