src/Tools/jEdit/src/scala_console.scala
changeset 48412 dbd75cbb84ba
parent 48409 0d2114eb412a
child 48613 232652ac346e
equal deleted inserted replaced
48411:5b3440850d36 48412:dbd75cbb84ba
    28 
    28 
    29   private def reconstruct_classpath(): String =
    29   private def reconstruct_classpath(): String =
    30   {
    30   {
    31     def find_jars(start: String): List[String] =
    31     def find_jars(start: String): List[String] =
    32       if (start != null)
    32       if (start != null)
    33         Standard_System.find_files(new JFile(start),
    33         File.find_files(new JFile(start),
    34           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    34           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    35       else Nil
    35       else Nil
    36     val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
    36     val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
    37     path.mkString(JFile.pathSeparator)
    37     path.mkString(JFile.pathSeparator)
    38   }
    38   }