--- 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\")")
--- 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