equal
deleted
inserted
replaced
37 |
37 |
38 store.try_open_database(session_name) match { |
38 store.try_open_database(session_name) match { |
39 case None => no_timings |
39 case None => no_timings |
40 case Some(db) => |
40 case Some(db) => |
41 def ignore_error(msg: String) = { |
41 def ignore_error(msg: String) = { |
42 progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg)) |
42 progress.echo_warning("Ignoring bad database " + db + |
|
43 " for session " + quote(session_name) + (if (msg == "") "" else ":\n" + msg)) |
43 no_timings |
44 no_timings |
44 } |
45 } |
45 try { |
46 try { |
46 val command_timings = store.read_command_timings(db, session_name) |
47 val command_timings = store.read_command_timings(db, session_name) |
47 val session_timing = |
48 val session_timing = |