src/Pure/General/path.scala
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]