author | wenzelm |
Thu, 10 Dec 2020 22:46:12 +0100 | |
changeset 72880 | 2fce0ce47627 |
parent 72879 | b3e9e9e4ff74 |
child 72881 | 220a094a42d8 |
--- a/src/Pure/Thy/presentation.scala Thu Dec 10 22:44:53 2020 +0100 +++ b/src/Pure/Thy/presentation.scala Thu Dec 10 22:46:12 2020 +0100 @@ -60,7 +60,7 @@ def log: String = log_xz.uncompress().text def log_lines: List[String] = split_lines(log) - def write(db: SQL.Database, session_name: String) = + def write(db: SQL.Database, session_name: String): Unit = write_document(db, session_name, this) }