tuned: drop pointless SQL.order_by (see also 5f706f7c624b);
authorwenzelm
Sat, 09 Mar 2024 13:06:13 +0100
changeset 79827 e38f5f81592d
parent 79826 487137973a8d
child 79828 5969ead9f900
tuned: drop pointless SQL.order_by (see also 5f706f7c624b);
src/Pure/Build/build_process.scala
--- 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)