changeset 80492 | 43323d886ea3 |
parent 75702 | 97e8f4c938bf |
child 80507 | 8e4731a2a041 |
--- a/src/Tools/jEdit/jedit_main/scala_console.scala Wed Jul 03 20:18:36 2024 +0200 +++ b/src/Tools/jEdit/jedit_main/scala_console.scala Wed Jul 03 20:35:10 2024 +0200 @@ -50,7 +50,7 @@ override def flush(): Unit = { val s = buf.synchronized { val s = buf.toString; buf.clear(); s } - val str = UTF8.decode_permissive(s) + val str = UTF8.decode_permissive(Bytes.raw(s)) GUI_Thread.later { if (global_out == null) java.lang.System.out.print(str) else global_out.writeAttrs(null, str)