diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/General/path.scala
--- 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]