# HG changeset patch
# User wenzelm
# Date 1716631777 -7200
# Node ID 79655411a32df7f5ff5af30bdf2583d146b82351
# Parent  ed8a3f4e3de732924dfbdbc9bce6d658d10191e7
clarified signature (see also be0ab4b94c62 and c41791ad75c3);

diff -r ed8a3f4e3de7 -r 79655411a32d src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Fri May 24 20:23:14 2024 +0200
+++ b/src/Pure/Build/sessions.scala	Sat May 25 12:09:37 2024 +0200
@@ -1235,7 +1235,7 @@
     ssh.is_file(dir + ROOT) || ssh.is_file(dir + ROOTS)
 
   def check_session_dir(dir: Path): Path =
-    if (is_session_dir(dir)) File.pwd() + dir.expand
+    if (is_session_dir(dir)) dir.absolute
     else {
       error("Bad session root directory: " + dir.expand.toString +
         "\n  (missing \"ROOT\" or \"ROOTS\")")
diff -r ed8a3f4e3de7 -r 79655411a32d src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri May 24 20:23:14 2024 +0200
+++ b/src/Pure/General/file.scala	Sat May 25 12:09:37 2024 +0200
@@ -81,8 +81,6 @@
   def path(file: JFile): Path = Path.explode(standard_path(file))
   def path(java_path: JPath): Path = path(java_path.toFile)
 
-  def pwd(): Path = path(Path.current.absolute_file)
-
   def uri(file: JFile): URI = file.toURI
   def uri(path: Path): URI = path.file.toURI