# HG changeset patch
# User wenzelm
# Date 1579090936 -3600
# Node ID e40f287c25c4d033bcaf08d9e9ec13d93abffc67
# Parent  26801434d62897c024099d150fd08ab5e9ad7c62
unused;

diff -r 26801434d628 -r e40f287c25c4 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jan 14 16:03:31 2020 +0100
+++ b/src/Pure/General/file.scala	Wed Jan 15 13:22:16 2020 +0100
@@ -118,9 +118,6 @@
     else None
   }
 
-  def rebase_path(base: Path, other: Path): Option[Path] =
-    relative_path(base, other).map(base + _)
-
 
   /* bash path */