src/Pure/Tools/build.scala
changeset 65320 52861eebf58d
parent 65318 342efc382558
child 65344 b99283eed13c
     1.1 --- a/src/Pure/Tools/build.scala	Sun Mar 19 12:57:29 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Mar 19 13:05:06 2017 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4            try {
     1.5              using(SQLite.open_database(database))(db =>
     1.6              {
     1.7 -              val build_log = store.read_build_log(db, command_timings = true)
     1.8 +              val build_log = store.read_build_log(db, name, command_timings = true)
     1.9                val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    1.10                (build_log.command_timings, session_timing)
    1.11              })
    1.12 @@ -525,7 +525,7 @@
    1.13                  {
    1.14                    store.find_database_heap(name) match {
    1.15                      case Some((database, heap_stamp)) =>
    1.16 -                      using(SQLite.open_database(database))(store.read_build(_)) match {
    1.17 +                      using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.18                          case Some(build) =>
    1.19                            val current =
    1.20                              build.sources == sources_stamp(name) &&