author | wenzelm |
Sat, 26 May 2018 21:24:07 +0200 | |
changeset 68294 | 0f513ae3db77 |
parent 68293 | 2bc4e5d9cca6 |
child 68295 | 781a98696638 |
--- a/src/Pure/Thy/sessions.scala Sat May 26 21:23:51 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Sat May 26 21:24:07 2018 +0200 @@ -1092,8 +1092,8 @@ /* SQL database content */ - val xml_cache = XML.make_cache() - val xz_cache = XZ.make_cache() + val xml_cache: XML.Cache = XML.make_cache() + val xz_cache: XZ.Cache = XZ.make_cache() def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = db.using_statement(Session_Info.table.select(List(column),