author | wenzelm |
Fri, 07 Jul 2023 14:10:36 +0200 | |
changeset 78262 | 968b5b981a8c |
parent 78261 | 316afcb8dc0c |
child 78263 | 8c999990262c |
--- a/src/Pure/Thy/store.scala Fri Jul 07 14:08:53 2023 +0200 +++ b/src/Pure/Thy/store.scala Fri Jul 07 14:10:36 2023 +0200 @@ -132,7 +132,7 @@ build_log: Build_Log.Session_Info, build: Build_Info ): Unit = { - db.execute_statement(Data.Session_Info.table.insert(), body = + db.execute_statement(Session_Info.table.insert(), body = { stmt => stmt.string(1) = session_name stmt.bytes(2) = Properties.encode(build_log.session_timing)