# HG changeset patch
# User wenzelm
# Date 1398773050 -7200
# Node ID afaec818fcfd3fa9f361b67ecdc94e437261a9b6
# Parent  433cf57550fa4d653a0b164fd3368ae6673f7f53
ignore malformed file names outright, e.g. .class files with dollar;

diff -r 433cf57550fa -r afaec818fcfd 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 */