Tue, 02 Jul 2024 23:29:46 +0200 enforce rebuild of Isabelle/ML; default tip
wenzelm [Tue, 02 Jul 2024 23:29:46 +0200] rev 80482
enforce rebuild of Isabelle/ML;
Tue, 02 Jul 2024 23:28:55 +0200 more uniform Bytes.read_stream vs. File.read_stream;
wenzelm [Tue, 02 Jul 2024 23:28:55 +0200] rev 80481
more uniform Bytes.read_stream vs. File.read_stream;
Tue, 02 Jul 2024 23:13:35 +0200 clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm [Tue, 02 Jul 2024 23:13:35 +0200] rev 80480
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
Tue, 02 Jul 2024 22:38:00 +0200 more specialized operations;
wenzelm [Tue, 02 Jul 2024 22:38:00 +0200] rev 80479
more specialized operations;
Tue, 02 Jul 2024 21:54:12 +0200 notable performance tuning for Library.separated_chunks variants;
wenzelm [Tue, 02 Jul 2024 21:54:12 +0200] rev 80478
notable performance tuning for Library.separated_chunks variants; more direct NoSuchElementException;
Tue, 02 Jul 2024 21:35:40 +0200 tuned;
wenzelm [Tue, 02 Jul 2024 21:35:40 +0200] rev 80477
tuned;
Tue, 02 Jul 2024 17:38:28 +0200 only consider jobs late if they have ancestors (amending 12901c03b416);
Fabian Huch <huch@in.tum.de> [Tue, 02 Jul 2024 17:38:28 +0200] rev 80476
only consider jobs late if they have ancestors (amending 12901c03b416);
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 tip