Wed, 20 Feb 2013 19:57:17 +0100 option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
wenzelm [Wed, 20 Feb 2013 19:57:17 +0100] rev 51230
option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
Wed, 20 Feb 2013 18:04:44 +0100 prefer outdegree in comparison again (cf. 88c96e836ed6) -- NB: big jobs might hide behind small ones in this naive queuing scheme;
wenzelm [Wed, 20 Feb 2013 18:04:44 +0100] rev 51229
prefer outdegree in comparison again (cf. 88c96e836ed6) -- NB: big jobs might hide behind small ones in this naive queuing scheme;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip