Wed, 13 Mar 2024 11:23:22 +0100 | wenzelm | proper system option, instead of hardwired default; | changeset | files |
Wed, 13 Mar 2024 11:04:06 +0100 | wenzelm | tuned signature: fewer warnings in IntelliJ IDEA; | changeset | files |
Wed, 13 Mar 2024 10:58:15 +0100 | wenzelm | tuned comments; | changeset | files |
Wed, 13 Mar 2024 11:54:06 +0100 | Fabian Huch | clarified build schedule host: proper module; | changeset | files |
Wed, 13 Mar 2024 11:45:20 +0100 | Fabian Huch | remove unused dummy; | changeset | files |
Wed, 13 Mar 2024 11:05:53 +0100 | Fabian Huch | tuned; | changeset | files |
Tue, 12 Mar 2024 13:52:29 +0100 | Fabian Huch | use timeout as default build time predictor if no data is available; | changeset | files |
Tue, 12 Mar 2024 16:20:02 +0000 | paulson | merged | changeset | files |