src/Tools/jEdit/jedit_main/scala_console.scala
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)