author | wenzelm |
Sun, 10 Jan 2010 21:08:23 +0100 | |
changeset 34857 | d3cffc4241f2 |
parent 34856 | aa9e22d9f9a7 |
child 34858 | ad486bd8abf3 |
--- a/src/Tools/jEdit/src/jedit/scala_console.scala Sun Jan 10 20:38:23 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala Sun Jan 10 21:08:23 2010 +0100 @@ -97,8 +97,6 @@ override def openConsole(console: Console) { - console.getOutputPane.getCaret.setBlinkRate(0) // FIXME property!? - val settings = new GenericRunnerSettings(report_error) settings.classpath.value = reconstruct_classpath()