Wed, 13 Mar 2024 11:23:22 +0100 proper system option, instead of hardwired default;
wenzelm [Wed, 13 Mar 2024 11:23:22 +0100] rev 79883
proper system option, instead of hardwired default;
Wed, 13 Mar 2024 11:04:06 +0100 tuned signature: fewer warnings in IntelliJ IDEA;
wenzelm [Wed, 13 Mar 2024 11:04:06 +0100] rev 79882
tuned signature: fewer warnings in IntelliJ IDEA;
Wed, 13 Mar 2024 10:58:15 +0100 tuned comments;
wenzelm [Wed, 13 Mar 2024 10:58:15 +0100] rev 79881
tuned comments;
Wed, 13 Mar 2024 11:54:06 +0100 clarified build schedule host: proper module;
Fabian Huch <huch@in.tum.de> [Wed, 13 Mar 2024 11:54:06 +0100] rev 79880
clarified build schedule host: proper module;
Wed, 13 Mar 2024 11:45:20 +0100 remove unused dummy;
Fabian Huch <huch@in.tum.de> [Wed, 13 Mar 2024 11:45:20 +0100] rev 79879
remove unused dummy;
Wed, 13 Mar 2024 11:05:53 +0100 tuned;
Fabian Huch <huch@in.tum.de> [Wed, 13 Mar 2024 11:05:53 +0100] rev 79878
tuned;
Tue, 12 Mar 2024 13:52:29 +0100 use timeout as default build time predictor if no data is available;
Fabian Huch <huch@in.tum.de> [Tue, 12 Mar 2024 13:52:29 +0100] rev 79877
use timeout as default build time predictor if no data is available;
Tue, 12 Mar 2024 16:20:02 +0000 merged
paulson [Tue, 12 Mar 2024 16:20:02 +0000] rev 79876
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 tip