changeset 77182 | 25dbf5bec91e |
parent 76593 | badb5264f7b9 |
child 77286 | 6435b0fd48b5 |
--- a/src/Pure/General/logger.scala Fri Feb 03 14:29:07 2023 +0100 +++ b/src/Pure/General/logger.scala Fri Feb 03 16:24:46 2023 +0100 @@ -33,3 +33,9 @@ override def toString: String = path.toString } + +class System_Logger extends Logger { + def apply(msg: => String): Unit = + if (Platform.is_windows) System.out.println(msg) + else System.console.writer.println(msg) +}