src/Pure/Tools/main.scala
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)