author | wenzelm |
Tue, 05 Mar 2024 15:58:45 +0100 | |
changeset 79776 | c3f07c950116 |
parent 79775 | 752806151432 |
child 79777 | db9c6be8e236 |
--- a/src/Pure/General/logger.scala Tue Mar 05 15:54:33 2024 +0100 +++ b/src/Pure/General/logger.scala Tue Mar 05 15:58:45 2024 +0100 @@ -14,7 +14,7 @@ case None => No_Logger } - def make_progress(progress: Progress, guard_time: Time = Time.min): Logger = + def make_progress(progress: => Progress, guard_time: Time = Time.min): Logger = new Logger { override def output(msg: => String): Unit = if (progress != null) progress.echo(msg)