changeset 43605 | 4f119a9ed37c |
parent 43604 | ff33fea12337 |
child 43652 | dcd0b667f73d |
--- a/src/Pure/General/path.scala Thu Jun 30 14:03:31 2011 +0200 +++ b/src/Pure/General/path.scala Thu Jun 30 14:51:32 2011 +0200 @@ -102,7 +102,7 @@ def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root] def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } - def +(other: Path): Path = Path((elems :\ other.elems)(Path.apply_elem)) + def +(other: Path): Path = Path((other.elems :\ elems)(Path.apply_elem)) /* implode */