ignore malformed file names outright, e.g. .class files with dollar;
authorwenzelm
Tue, 29 Apr 2014 14:04:10 +0200
changeset 56783 afaec818fcfd
parent 56782 433cf57550fa
child 56784 776890e0cf71
ignore malformed file names outright, e.g. .class files with dollar;
src/Pure/General/file.scala
--- 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 */