changeset 46712 | 8650d9a95736 |
parent 45244 | c149b61bc372 |
child 47661 | 012a887997f3 |
--- a/src/Pure/General/path.scala Mon Feb 27 16:56:25 2012 +0100 +++ b/src/Pure/General/path.scala Mon Feb 27 17:13:25 2012 +0100 @@ -98,7 +98,7 @@ } -class Path private(private val elems: List[Path.Elem]) // reversed elements +final class Path private(private val elems: List[Path.Elem]) // reversed elements { def is_current: Boolean = elems.isEmpty def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]