--- a/src/Pure/Thy/export.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/export.scala Mon Mar 01 22:22:12 2021 +0100
@@ -116,7 +116,7 @@
def uncompressed_yxml: XML.Body =
YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
- def write(db: SQL.Database)
+ def write(db: SQL.Database): Unit =
{
val (compressed, bytes) = body.join
db.using_statement(Data.table.insert())(stmt =>
@@ -339,7 +339,7 @@
progress: Progress = new Progress,
export_prune: Int = 0,
export_list: Boolean = false,
- export_patterns: List[String] = Nil)
+ export_patterns: List[String] = Nil): Unit =
{
using(store.open_database(session_name))(db =>
{