changeset 80507 | 8e4731a2a041 |
parent 80492 | 43323d886ea3 |
--- a/src/Tools/jEdit/jedit_main/scala_console.scala Fri Jul 05 00:21:47 2024 +0200 +++ b/src/Tools/jEdit/jedit_main/scala_console.scala Fri Jul 05 10:55:02 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(Bytes.raw(s)) + val str = Bytes.raw(s).text GUI_Thread.later { if (global_out == null) java.lang.System.out.print(str) else global_out.writeAttrs(null, str)