Thu, 06 Aug 2020 23:44:43 +0200 | wenzelm | recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a); | changeset | files |
Thu, 06 Aug 2020 23:27:52 +0200 | wenzelm | more compact command_timings, as in former batch-build; | changeset | files |