--- a/src/Pure/General/logger.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/logger.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,12 +23,12 @@
object No_Logger extends Logger
{
- def apply(msg: => String) { }
+ def apply(msg: => String): Unit = {}
}
class File_Logger(path: Path) extends Logger
{
- def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } }
+ def apply(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }
override def toString: String = path.toString
}