src/Pure/Tools/build.scala
changeset 65935 73c099fa96a4
parent 65832 2fb85623c386
child 66571 0fdeb24e535e
     1.1 --- a/src/Pure/Tools/build.scala	Fri May 26 15:19:21 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri May 26 15:28:46 2017 +0200
     1.3 @@ -51,9 +51,13 @@
     1.4            try {
     1.5              using(SQLite.open_database(database))(db =>
     1.6              {
     1.7 -              val build_log = store.read_build_log(db, name, command_timings = true)
     1.8 -              val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
     1.9 -              (build_log.command_timings, session_timing)
    1.10 +              val command_timings = store.read_command_timings(db, name)
    1.11 +              val session_timing =
    1.12 +                store.read_session_timing(db, name) match {
    1.13 +                  case Markup.Elapsed(t) => t
    1.14 +                  case _ => 0.0
    1.15 +                }
    1.16 +              (command_timings, session_timing)
    1.17              })
    1.18            }
    1.19            catch {