src/Pure/Build/build_schedule.scala
changeset 79834 45b81ff3c972
parent 79832 2a3c0a68221c
child 79835 866d96915388
equal deleted inserted replaced
79833:d71af537a6e9 79834:45b81ff3c972
  1207       val running_builds_domain =
  1207       val running_builds_domain =
  1208         db.execute_query_statement(
  1208         db.execute_query_statement(
  1209           Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.undefined)),
  1209           Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.undefined)),
  1210           Map.from[String, Unit], res => res.string(Base.build_uuid) -> ())
  1210           Map.from[String, Unit], res => res.string(Base.build_uuid) -> ())
  1211 
  1211 
  1212       val update =
  1212       val update = Library.Update.make(read_scheduled_builds_domain(db), running_builds_domain)
  1213         Build_Process.data_update(read_scheduled_builds_domain(db), running_builds_domain)
       
  1214 
  1213 
  1215       remove_schedules(db, update.delete)
  1214       remove_schedules(db, update.delete)
  1216     }
  1215     }
  1217 
  1216 
  1218     override val tables: SQL.Tables = SQL.Tables(Schedules.table, Nodes.table)
  1217     override val tables: SQL.Tables = SQL.Tables(Schedules.table, Nodes.table)