src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/General/file.scala	Wed Feb 12 14:28:32 2025 +0100
@@ -123,6 +123,9 @@
     else None
   }
 
+  def perhaps_relative_path(base: Path, other: Path): Path =
+    relative_path(base, other).getOrElse(other)
+
 
   /* bash path */