src/Pure/System/bash.scala
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
               }