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);
Tue, 02 Jul 2024 16:42:13 +0200 enforce rebuild of Isabelle/ML;
wenzelm [Tue, 02 Jul 2024 16:42:13 +0200] rev 80475
enforce rebuild of Isabelle/ML;
Tue, 02 Jul 2024 16:36:49 +0200 misc tuning: more uniform read_stream vs. read_file;
wenzelm [Tue, 02 Jul 2024 16:36:49 +0200] rev 80474
misc tuning: more uniform read_stream vs. read_file;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 tip