clarified signature (see also be0ab4b94c62 and c41791ad75c3);
authorwenzelm
Sat, 25 May 2024 12:09:37 +0200
changeset 80194 79655411a32d
parent 80193 ed8a3f4e3de7
child 80195 e2ccabd7a857
clarified signature (see also be0ab4b94c62 and c41791ad75c3);
src/Pure/Build/sessions.scala
src/Pure/General/file.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\")")
--- 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