equal
deleted
inserted
replaced
71 |
71 |
72 update_environment() |
72 update_environment() |
73 |
73 |
74 System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) |
74 System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) |
75 System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) |
75 System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) |
|
76 System.setProperty("scala.color", "false") |
76 |
77 |
77 val jedit = |
78 val jedit = |
78 Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) |
79 Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) |
79 val jedit_main = jedit.getMethod("main", classOf[Array[String]]) |
80 val jedit_main = jedit.getMethod("main", classOf[Array[String]]) |
80 |
81 |