src/Pure/General/file.scala
changeset 76546 88cecb9f1cdc
parent 76540 83de6e9ae983
child 76884 a004c5322ea4
--- a/src/Pure/General/file.scala	Wed Nov 30 15:53:21 2022 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 30 21:36:06 2022 +0100
@@ -61,6 +61,8 @@
   def canonical_name(file: JFile): String = canonical(file).getPath
 
   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