src/Pure/Admin/build_status.scala
changeset 65804 73ed0ebac3b0
parent 65799 ed705d6a6a63
child 65835 5ec497351636
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed May 10 22:30:28 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Fri May 12 11:56:41 2017 +0200
     1.3 @@ -30,17 +30,13 @@
     1.4  
     1.5      def select(options: Options, columns: List[SQL.Column], only_sessions: Set[String]): SQL.Source =
     1.6      {
     1.7 -      val sql_sessions =
     1.8 -        if (only_sessions.isEmpty) ""
     1.9 -        else
    1.10 -          only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
    1.11 -            .mkString("(", " OR ", ") AND ")
    1.12 -
    1.13        Build_Log.Data.universal_table.select(columns, distinct = true,
    1.14          sql = "WHERE " +
    1.15            Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days(options)) + " AND " +
    1.16            Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
    1.17 -          " AND " + sql_sessions + SQL.enclose(sql) +
    1.18 +          (if (only_sessions.isEmpty) ""
    1.19 +           else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
    1.20 +          " AND " + SQL.enclose(sql) +
    1.21            " ORDER BY " + Build_Log.Data.pull_date + " DESC")
    1.22      }
    1.23    }