# HG changeset patch
# User wenzelm
# Date 1397395923 -7200
# Node ID 347d7feae8d551a9c2afec8f129f9691e5011251
# Parent  1afb78a933768fc128c2a6eb1eb47b3b1dcda5c5
clarified according to ML version;

diff -r 1afb78a93376 -r 347d7feae8d5 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat Apr 12 21:59:30 2014 +0200
+++ b/src/Pure/General/path.scala	Sun Apr 13 15:32:03 2014 +0200
@@ -165,7 +165,7 @@
     val (prefix, base) = split_path
     base match {
       case Ext(b, e) => (prefix + Path.basic(b), e)
-      case _ => (Path.basic(base), "")
+      case _ => (prefix + Path.basic(base), "")
     }
   }