| changeset 65875 | 12c90c0c4b32 |
| parent 63749 | 4fe8cfaeb1fc |
| child 66463 | 934bd55d768a |
--- a/src/Pure/Tools/main.scala Fri May 19 16:43:11 2017 +0200 +++ b/src/Pure/Tools/main.scala Fri May 19 18:10:19 2017 +0200 @@ -73,6 +73,7 @@ System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) + System.setProperty("scala.color", "false") val jedit = Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)