src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/General/file.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -68,8 +68,8 @@
 
   def relative_path(base: Path, other: Path): Option[Path] =
   {
-    val base_path = base.file.toPath
-    val other_path = other.file.toPath
+    val base_path = base.java_path
+    val other_path = other.java_path
     if (other_path.startsWith(base_path))
       Some(path(base_path.relativize(other_path).toFile))
     else None