# HG changeset patch
# User wenzelm
# Date 1709581786 -3600
# Node ID 52b5c7c8e6d9df5d0d9cef043c826f98e38829f7
# Parent  feec445a82c3470ded0c63db3dd9b336c3910de2
more robust handling of uninitialized value, notably Build_Process.progress;

diff -r feec445a82c3 -r 52b5c7c8e6d9 src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Mon Mar 04 19:14:16 2024 +0100
+++ b/src/Pure/General/logger.scala	Mon Mar 04 20:49:46 2024 +0100
@@ -12,7 +12,7 @@
     log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
 
   def make(progress: Progress): Logger =
-    new Logger { def apply(msg: => String): Unit = progress.echo(msg) }
+    new Logger { def apply(msg: => String): Unit = if (progress != null) progress.echo(msg) }
 
   def make_system_log(progress: Progress, options: Options): Logger =
     options.string("system_log") match {