# HG changeset patch
# User wenzelm
# Date 1607636772 -3600
# Node ID 2fce0ce47627ed286d76f8ad1e87bada5ecf93b9
# Parent  b3e9e9e4ff74f49b162c48f61e7e70a4396e0227
tuned;

diff -r b3e9e9e4ff74 -r 2fce0ce47627 src/Pure/Thy/presentation.scala
--- 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)
   }