updated File.find_files;
authorwenzelm
Fri, 20 Jul 2012 23:37:54 +0200
changeset 49427dbd75cbb84ba
parent 49426 5b3440850d36
child 49428 3e730188f328
updated File.find_files;
src/Tools/jEdit/src/scala_console.scala
     1.1 --- a/src/Tools/jEdit/src/scala_console.scala	Fri Jul 20 23:16:54 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Fri Jul 20 23:37:54 2012 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4    {
     1.5      def find_jars(start: String): List[String] =
     1.6        if (start != null)
     1.7 -        Standard_System.find_files(new JFile(start),
     1.8 +        File.find_files(new JFile(start),
     1.9            entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    1.10        else Nil
    1.11      val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)