author | wenzelm |
Sat, 09 Mar 2024 13:06:13 +0100 | |
changeset 79827 | e38f5f81592d |
parent 79826 | 487137973a8d |
child 79828 | 5969ead9f900 |
--- a/src/Pure/Build/build_process.scala Sat Mar 09 12:06:08 2024 +0100 +++ b/src/Pure/Build/build_process.scala Sat Mar 09 13:06:13 2024 +0100 @@ -620,7 +620,7 @@ def read_running(db: SQL.Database): State.Running = db.execute_query_statement( - Running.table.select(sql = SQL.order_by(List(Running.name))), + Running.table.select(), Map.from[String, Job], { res => val name = res.string(Running.name)