equal
deleted
inserted
replaced
122 timing.change { |
122 timing.change { |
123 case None => |
123 case None => |
124 if (timing_file.isFile) { |
124 if (timing_file.isFile) { |
125 val t = |
125 val t = |
126 Word.explode(File.read(timing_file)) match { |
126 Word.explode(File.read(timing_file)) match { |
127 case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) => |
127 case List(Value.Long(elapsed), Value.Long(cpu)) => |
128 Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
128 Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
129 case _ => Timing.zero |
129 case _ => Timing.zero |
130 } |
130 } |
131 timing_file.delete |
131 timing_file.delete |
132 Some(t) |
132 Some(t) |