ignore malformed file names outright, e.g. .class files with dollar;
--- a/src/Pure/General/file.scala Tue Apr 29 13:32:13 2014 +0200
+++ b/src/Pure/General/file.scala Tue Apr 29 14:04:10 2014 +0200
@@ -28,10 +28,12 @@
}
def find_files(dir: Path): Stream[Path] =
- read_dir(dir).toStream.map(name => {
- val path = dir + Path.basic(name)
- path #:: (if (path.is_dir) find_files(path) else Stream.empty)
- }).flatten
+ read_dir(dir).toStream.map(name =>
+ if (Path.is_wellformed(name)) {
+ val path = dir + Path.basic(name)
+ path #:: (if (path.is_dir) find_files(path) else Stream.empty)
+ }
+ else Stream.empty).flatten
/* read */