changeset 63805 | c272680df665 |
parent 62610 | 4c89504c76fb |
child 63996 | 3f47fec9edfc |
--- a/src/Pure/System/bash.scala Mon Sep 05 21:09:50 2016 +0200 +++ b/src/Pure/System/bash.scala Mon Sep 05 22:09:52 2016 +0200 @@ -124,7 +124,7 @@ if (timing_file.isFile) { val t = Word.explode(File.read(timing_file)) match { - case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) => + case List(Value.Long(elapsed), Value.Long(cpu)) => Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) case _ => Timing.zero }