# HG changeset patch # User wenzelm # Date 1489784231 -3600 # Node ID dfbb1743034256f241e47c32e4e04cc43fba34ed # Parent a71db30f3b2d0e68deb3463f1a5d516dbb24ac00 proper columns; diff -r a71db30f3b2d -r dfbb17430342 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Mar 17 21:55:13 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Mar 17 21:57:11 2017 +0100 @@ -684,7 +684,7 @@ } def read_build(db: SQL.Database): Option[Build.Session_Info] = - using(db.select_statement(Session_Info.table, Session_Info.table.columns))(stmt => + using(db.select_statement(Session_Info.table, Session_Info.build_columns))(stmt => { val rs = stmt.executeQuery if (!rs.next) None