# HG changeset patch
# User wenzelm
# Date 1495210219 -7200
# Node ID 12c90c0c4b323db80937a84c84d05a7cae5fd1a6
# Parent  bd45c8ebc214de6276a1ddf0cbdeab2fe1404870
suppress ANSI control sequences in Scala console;

diff -r bd45c8ebc214 -r 12c90c0c4b32 src/Pure/Tools/main.scala
--- 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)