equal
deleted
inserted
replaced
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 } |