# HG changeset patch
# User wenzelm
# Date 1709652040 -3600
# Node ID 42c3e6dc57d91c764a1937093bd2481226fcd52c
# Parent  db9c6be8e236dad55e14586cabb5079762fccc27
more robust, notably for remote process (via SSH);

diff -r db9c6be8e236 -r 42c3e6dc57d9 src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Tue Mar 05 16:06:06 2024 +0100
+++ b/src/Pure/General/logger.scala	Tue Mar 05 16:20:40 2024 +0100
@@ -51,7 +51,13 @@
 class System_Logger(override val guard_time: Time = Time.min)
 extends Logger {
   override def output(msg: => String): Unit = synchronized {
-    if (Platform.is_windows) System.out.println(msg)
-    else System.console.writer.println(msg)
+    if (System.console != null && System.console.writer != null) {
+      System.console.writer.println(msg)
+      System.console.writer.flush()
+    }
+    else if (System.out != null) {
+      System.out.println(msg)
+      System.out.flush()
+    }
   }
 }