diff -r fd487d261169 -r 5036edb025b7 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Sat Apr 04 18:05:37 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Sat Apr 04 18:13:05 2020 +0200
@@ -64,7 +64,7 @@
         if (global_out == null) System.out.print(str)
         else global_out.writeAttrs(null, str)
       }
-      Thread.sleep(10)  // FIXME adhoc delay to avoid loosing output
+      Time.seconds(0.01).sleep  // FIXME adhoc delay to avoid loosing output
     }
 
     override def close() { flush () }