src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Tue Feb 18 18:43:31 2014 +0100
+++ b/src/Pure/General/path.scala	Tue Feb 18 18:43:47 2014 +0100
@@ -94,7 +94,7 @@
       else (List(root_elem(es.head)), es.tail)
     val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
 
-    new Path(norm_elems(elems.reverse ++ roots))
+    new Path(norm_elems(elems.reverse ::: roots))
   }
 
   def is_ok(str: String): Boolean =