# HG changeset patch
# User wenzelm
# Date 1364415933 -3600
# Node ID bfdc3f720bd64aed9258336cc90aca0beedee2a7
# Parent  3f4ecbd9e5fa3cec81ccef739be28137a29ca800
discontinued obsolete parallel_proofs_reuse_timing;

diff -r 3f4ecbd9e5fa -r bfdc3f720bd6 etc/options
--- a/etc/options	Wed Mar 27 21:13:02 2013 +0100
+++ b/etc/options	Wed Mar 27 21:25:33 2013 +0100
@@ -55,8 +55,6 @@
   -- "upper bound for forks of nested proofs (multiplied by worker threads)"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
-option parallel_proofs_reuse_timing : bool = true
-  -- "reuse timing information from old log file for parallel proof scheduling"
 
 
 section "Detail of Proof Recording"
diff -r 3f4ecbd9e5fa -r bfdc3f720bd6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 27 21:13:02 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 27 21:25:33 2013 +0100
@@ -326,10 +326,7 @@
 
       val timings =
         sessions.par.map((name: String) =>
-          Exn.capture {
-            if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
-            else (name, (Nil, 0.0))
-          }).toList.map(Exn.release(_))
+          Exn.capture { (name, load_timings(name)) }).toList.map(Exn.release(_))
       val command_timings =
         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
       val session_timing =